From 1011d3191cfeec3177ec1dce8e1772c3b75b8cbd Mon Sep 17 00:00:00 2001
From: jo-hanna1997 <stu203549@mail.uni-kiel.de>
Date: Tue, 23 Jun 2020 11:12:46 +0200
Subject: [PATCH 01/16] Define functions, datatypes and properties in Haskell

---
 .../FastAndLooseReasoning.hs                  | 38 +++++++++++++++++++
 1 file changed, 38 insertions(+)
 create mode 100644 example/CaseStudyMorallyCorrect/FastAndLooseReasoning.hs

diff --git a/example/CaseStudyMorallyCorrect/FastAndLooseReasoning.hs b/example/CaseStudyMorallyCorrect/FastAndLooseReasoning.hs
new file mode 100644
index 00000000..09f7bf61
--- /dev/null
+++ b/example/CaseStudyMorallyCorrect/FastAndLooseReasoning.hs
@@ -0,0 +1,38 @@
+module FastLooseBasic where
+
+import           Test.QuickCheck
+
+data Peano = Zero | S Peano
+
+reverse :: [a] -> [a]
+reverse xs = rev [] xs
+
+rev acc []       = acc
+rev acc (x : xs) = rev (x : acc) xs
+
+map :: (a -> b) -> [a] -> [b]
+map f []       = []
+map f (x : xs) = f x : map f xs
+
+comp :: (b -> c) -> (a -> b) -> a -> c
+comp g f a = g (f a)
+
+id :: a -> a
+id a = a
+
+plus :: Peano -> Peano -> Peano
+plus = foldPeano S
+
+minus :: Peano -> Peano -> Peano
+minus = foldPeano pred
+
+pred :: Peano -> Peano
+pred Zero  = Zero
+pred (S n) = n
+
+foldPeano :: (a -> a) -> a -> Peano -> a
+foldPeano f a Zero  = a
+foldPeano f a (S n) = f (foldPeano f a n)
+
+prop_rev_is_rev_inv :: [a] -> Property
+prop_rev_is_rev_inv xs = reverse (reverse xs) === xs

From 222f5087ecf8245aff9897f24e2169a9d51b6f88 Mon Sep 17 00:00:00 2001
From: jo-hanna1997 <stu203549@mail.uni-kiel.de>
Date: Tue, 23 Jun 2020 11:14:28 +0200
Subject: [PATCH 02/16] Translate Haskell version into Coq

---
 .../Output/FastLooseBasic.json                | 372 ++++++++++++++++++
 .../Output/FastLooseBasic.v                   | 144 +++++++
 2 files changed, 516 insertions(+)
 create mode 100644 example/CaseStudyMorallyCorrect/Output/FastLooseBasic.json
 create mode 100644 example/CaseStudyMorallyCorrect/Output/FastLooseBasic.v

diff --git a/example/CaseStudyMorallyCorrect/Output/FastLooseBasic.json b/example/CaseStudyMorallyCorrect/Output/FastLooseBasic.json
new file mode 100644
index 00000000..3594889d
--- /dev/null
+++ b/example/CaseStudyMorallyCorrect/Output/FastLooseBasic.json
@@ -0,0 +1,372 @@
+{
+    "type-synonyms": [],
+    "library-name": "Generated",
+    "exported-values": [
+        "FastLooseBasic.S",
+        "FastLooseBasic.Zero",
+        "FastLooseBasic.comp",
+        "FastLooseBasic.foldPeano",
+        "FastLooseBasic.id",
+        "FastLooseBasic.map",
+        "FastLooseBasic.minus",
+        "FastLooseBasic.plus",
+        "FastLooseBasic.pred",
+        "FastLooseBasic.prop_rev_is_rev_inv",
+        "FastLooseBasic.rev",
+        "FastLooseBasic.reverse"
+    ],
+    "module-name": "FastLooseBasic",
+    "exported-types": [
+        "FastLooseBasic.Peano"
+    ],
+    "constructors": [
+        {
+            "arity": 1,
+            "coq-smart-name": "S",
+            "haskell-type": "FastLooseBasic.Peano -> FastLooseBasic.Peano",
+            "coq-name": "s",
+            "haskell-name": "FastLooseBasic.S"
+        },
+        {
+            "arity": 0,
+            "coq-smart-name": "Zero",
+            "haskell-type": "FastLooseBasic.Peano",
+            "coq-name": "zero",
+            "haskell-name": "FastLooseBasic.Zero"
+        },
+        {
+            "arity": 0,
+            "coq-smart-name": "False_",
+            "haskell-type": "Prelude.Bool",
+            "coq-name": "false",
+            "haskell-name": "Prelude.False"
+        },
+        {
+            "arity": 0,
+            "coq-smart-name": "True_",
+            "haskell-type": "Prelude.Bool",
+            "coq-name": "true",
+            "haskell-name": "Prelude.True"
+        },
+        {
+            "arity": 0,
+            "coq-smart-name": "Tt",
+            "haskell-type": "Prelude.()",
+            "coq-name": "tt",
+            "haskell-name": "Prelude.()"
+        },
+        {
+            "arity": 2,
+            "coq-smart-name": "Pair_",
+            "haskell-type": "a -> b -> Prelude.(,) a b",
+            "coq-name": "pair_",
+            "haskell-name": "Prelude.(,)"
+        },
+        {
+            "arity": 2,
+            "coq-smart-name": "Cons",
+            "haskell-type": "a -> Prelude.([]) a -> Prelude.([]) a",
+            "coq-name": "cons",
+            "haskell-name": "Prelude.(:)"
+        },
+        {
+            "arity": 0,
+            "coq-smart-name": "Nil",
+            "haskell-type": "Prelude.([]) a",
+            "coq-name": "nil",
+            "haskell-name": "Prelude.([])"
+        }
+    ],
+    "types": [
+        {
+            "arity": 0,
+            "coq-name": "Peano",
+            "cons-names": [
+                "FastLooseBasic.Zero",
+                "FastLooseBasic.S"
+            ],
+            "haskell-name": "FastLooseBasic.Peano"
+        },
+        {
+            "arity": 0,
+            "coq-name": "Bool",
+            "cons-names": [
+                "Prelude.True",
+                "Prelude.False"
+            ],
+            "haskell-name": "Prelude.Bool"
+        },
+        {
+            "arity": 0,
+            "coq-name": "Integer",
+            "cons-names": [],
+            "haskell-name": "Prelude.Integer"
+        },
+        {
+            "arity": 0,
+            "coq-name": "Unit",
+            "cons-names": [
+                "Prelude.()"
+            ],
+            "haskell-name": "Prelude.()"
+        },
+        {
+            "arity": 2,
+            "coq-name": "Pair",
+            "cons-names": [
+                "Prelude.(,)"
+            ],
+            "haskell-name": "Prelude.(,)"
+        },
+        {
+            "arity": 1,
+            "coq-name": "List",
+            "cons-names": [
+                "Prelude.([])",
+                "Prelude.(:)"
+            ],
+            "haskell-name": "Prelude.([])"
+        },
+        {
+            "arity": 0,
+            "coq-name": "Property",
+            "cons-names": [],
+            "haskell-name": "Test.QuickCheck.Property"
+        }
+    ],
+    "version": 3,
+    "functions": [
+        {
+            "arity": 3,
+            "haskell-type": "(b -> c) -> (a -> b) -> a -> c",
+            "coq-name": "comp",
+            "needs-free-args": true,
+            "partial": false,
+            "haskell-name": "FastLooseBasic.comp"
+        },
+        {
+            "arity": 3,
+            "haskell-type": "(a -> a) -> a -> FastLooseBasic.Peano -> a",
+            "coq-name": "foldPeano",
+            "needs-free-args": true,
+            "partial": false,
+            "haskell-name": "FastLooseBasic.foldPeano"
+        },
+        {
+            "arity": 1,
+            "haskell-type": "a -> a",
+            "coq-name": "id",
+            "needs-free-args": true,
+            "partial": false,
+            "haskell-name": "FastLooseBasic.id"
+        },
+        {
+            "arity": 2,
+            "haskell-type": "(a -> b) -> Prelude.([]) a -> Prelude.([]) b",
+            "coq-name": "map",
+            "needs-free-args": true,
+            "partial": false,
+            "haskell-name": "FastLooseBasic.map"
+        },
+        {
+            "arity": 2,
+            "haskell-type": "FastLooseBasic.Peano -> FastLooseBasic.Peano -> FastLooseBasic.Peano",
+            "coq-name": "minus",
+            "needs-free-args": true,
+            "partial": false,
+            "haskell-name": "FastLooseBasic.minus"
+        },
+        {
+            "arity": 2,
+            "haskell-type": "FastLooseBasic.Peano -> FastLooseBasic.Peano -> FastLooseBasic.Peano",
+            "coq-name": "plus",
+            "needs-free-args": true,
+            "partial": false,
+            "haskell-name": "FastLooseBasic.plus"
+        },
+        {
+            "arity": 1,
+            "haskell-type": "FastLooseBasic.Peano -> FastLooseBasic.Peano",
+            "coq-name": "pred",
+            "needs-free-args": true,
+            "partial": false,
+            "haskell-name": "FastLooseBasic.pred"
+        },
+        {
+            "arity": 1,
+            "haskell-type": "Prelude.([]) a -> Test.QuickCheck.Property",
+            "coq-name": "prop_rev_is_rev_inv",
+            "needs-free-args": true,
+            "partial": false,
+            "haskell-name": "FastLooseBasic.prop_rev_is_rev_inv"
+        },
+        {
+            "arity": 2,
+            "haskell-type": "Prelude.([]) t0 -> Prelude.([]) t0 -> Prelude.([]) t0",
+            "coq-name": "rev",
+            "needs-free-args": true,
+            "partial": false,
+            "haskell-name": "FastLooseBasic.rev"
+        },
+        {
+            "arity": 1,
+            "haskell-type": "Prelude.([]) a -> Prelude.([]) a",
+            "coq-name": "reverse",
+            "needs-free-args": true,
+            "partial": false,
+            "haskell-name": "FastLooseBasic.reverse"
+        },
+        {
+            "arity": 1,
+            "haskell-type": "Prelude.Integer -> Prelude.Integer -> Prelude.Integer",
+            "coq-name": "negate",
+            "needs-free-args": true,
+            "partial": false,
+            "haskell-name": "Prelude.negate"
+        },
+        {
+            "arity": 2,
+            "haskell-type": "Prelude.Bool -> Prelude.Bool -> Prelude.Bool",
+            "coq-name": "andBool",
+            "needs-free-args": true,
+            "partial": false,
+            "haskell-name": "Prelude.(&&)"
+        },
+        {
+            "arity": 2,
+            "haskell-type": "Prelude.Integer -> Prelude.Integer -> Prelude.Integer",
+            "coq-name": "mulInteger",
+            "needs-free-args": true,
+            "partial": false,
+            "haskell-name": "Prelude.(*)"
+        },
+        {
+            "arity": 2,
+            "haskell-type": "Prelude.Integer -> Prelude.Integer -> Prelude.Integer",
+            "coq-name": "addInteger",
+            "needs-free-args": true,
+            "partial": false,
+            "haskell-name": "Prelude.(+)"
+        },
+        {
+            "arity": 2,
+            "haskell-type": "Prelude.Integer -> Prelude.Integer -> Prelude.Integer",
+            "coq-name": "subInteger",
+            "needs-free-args": true,
+            "partial": false,
+            "haskell-name": "Prelude.(-)"
+        },
+        {
+            "arity": 2,
+            "haskell-type": "Prelude.Integer -> Prelude.Integer -> Prelude.Bool",
+            "coq-name": "neqInteger",
+            "needs-free-args": true,
+            "partial": false,
+            "haskell-name": "Prelude.(/=)"
+        },
+        {
+            "arity": 2,
+            "haskell-type": "Prelude.Integer -> Prelude.Integer -> Prelude.Bool",
+            "coq-name": "ltInteger",
+            "needs-free-args": true,
+            "partial": false,
+            "haskell-name": "Prelude.(<)"
+        },
+        {
+            "arity": 2,
+            "haskell-type": "Prelude.Integer -> Prelude.Integer -> Prelude.Bool",
+            "coq-name": "leInteger",
+            "needs-free-args": true,
+            "partial": false,
+            "haskell-name": "Prelude.(<=)"
+        },
+        {
+            "arity": 2,
+            "haskell-type": "Prelude.Integer -> Prelude.Integer -> Prelude.Bool",
+            "coq-name": "eqInteger",
+            "needs-free-args": true,
+            "partial": false,
+            "haskell-name": "Prelude.(==)"
+        },
+        {
+            "arity": 2,
+            "haskell-type": "Prelude.Integer -> Prelude.Integer -> Prelude.Bool",
+            "coq-name": "gtInteger",
+            "needs-free-args": true,
+            "partial": false,
+            "haskell-name": "Prelude.(>)"
+        },
+        {
+            "arity": 2,
+            "haskell-type": "Prelude.Integer -> Prelude.Integer -> Prelude.Bool",
+            "coq-name": "geInteger",
+            "needs-free-args": true,
+            "partial": false,
+            "haskell-name": "Prelude.(>=)"
+        },
+        {
+            "arity": 2,
+            "haskell-type": "Prelude.Integer -> Prelude.Integer -> Prelude.Integer",
+            "coq-name": "powInteger",
+            "needs-free-args": true,
+            "partial": false,
+            "haskell-name": "Prelude.(^)"
+        },
+        {
+            "arity": 2,
+            "haskell-type": "Prelude.Bool -> Prelude.Bool -> Prelude.Bool",
+            "coq-name": "orBool",
+            "needs-free-args": true,
+            "partial": false,
+            "haskell-name": "Prelude.(||)"
+        },
+        {
+            "arity": 1,
+            "haskell-type": "Prelude.Bool -> Test.QuickCheck.Property",
+            "coq-name": "boolProp",
+            "needs-free-args": true,
+            "partial": false,
+            "haskell-name": "Test.QuickCheck.property"
+        },
+        {
+            "arity": 2,
+            "haskell-type": "Test.QuickCheck.Property -> Test.QuickCheck.Property -> Test.QuickCheck.Property",
+            "coq-name": "conjProp",
+            "needs-free-args": true,
+            "partial": false,
+            "haskell-name": "Test.QuickCheck.(.&&.)"
+        },
+        {
+            "arity": 2,
+            "haskell-type": "Test.QuickCheck.Property -> Test.QuickCheck.Property -> Test.QuickCheck.Property",
+            "coq-name": "disjProp",
+            "needs-free-args": true,
+            "partial": false,
+            "haskell-name": "Test.QuickCheck.(.||.)"
+        },
+        {
+            "arity": 2,
+            "haskell-type": "a -> a -> Test.QuickCheck.Property",
+            "coq-name": "neqProp",
+            "needs-free-args": true,
+            "partial": false,
+            "haskell-name": "Test.QuickCheck.(=/=)"
+        },
+        {
+            "arity": 2,
+            "haskell-type": "a -> a -> Test.QuickCheck.Property",
+            "coq-name": "eqProp",
+            "needs-free-args": true,
+            "partial": false,
+            "haskell-name": "Test.QuickCheck.(===)"
+        },
+        {
+            "arity": 2,
+            "haskell-type": "Prelude.Bool -> Test.QuickCheck.Property -> Test.QuickCheck.Property",
+            "coq-name": "preProp",
+            "needs-free-args": true,
+            "partial": false,
+            "haskell-name": "Test.QuickCheck.(==>)"
+        }
+    ]
+}
\ No newline at end of file
diff --git a/example/CaseStudyMorallyCorrect/Output/FastLooseBasic.v b/example/CaseStudyMorallyCorrect/Output/FastLooseBasic.v
new file mode 100644
index 00000000..beee1822
--- /dev/null
+++ b/example/CaseStudyMorallyCorrect/Output/FastLooseBasic.v
@@ -0,0 +1,144 @@
+(* module FastLooseBasic *)
+
+From Base Require Import Free.
+
+From Base Require Import Prelude.
+
+From Base Require Import Test.QuickCheck.
+
+(* Data type declarations for Peano *)
+
+Inductive Peano (Shape : Type) (Pos : Shape -> Type) : Type
+  := zero : Peano Shape Pos
+  |  s : Free Shape Pos (Peano Shape Pos) -> Peano Shape Pos.
+
+(* Arguments sentences for Peano *)
+
+Arguments zero {Shape} {Pos}.
+
+Arguments s {Shape} {Pos}.
+
+(* Smart constructors for Peano *)
+
+Definition Zero (Shape : Type) (Pos : Shape -> Type)
+   : Free Shape Pos (Peano Shape Pos) :=
+  pure zero.
+
+Definition S (Shape : Type) (Pos : Shape -> Type) (x_0
+    : Free Shape Pos (Peano Shape Pos))
+   : Free Shape Pos (Peano Shape Pos) :=
+  pure (s x_0).
+
+(* Helper functions for rev *)
+
+Fixpoint rev_0 (Shape : Type) (Pos : Shape -> Type) {t0 : Type} (a0
+                 : Free Shape Pos (List Shape Pos t0)) (a1 : List Shape Pos t0) {struct a1}
+           : Free Shape Pos (List Shape Pos t0)
+           := match a1 with
+              | nil => a0
+              | cons a2 a3 =>
+                  a3 >>=
+                  (fun (a3_0 : List Shape Pos t0) =>
+                     @rev_0 Shape Pos t0 (@Cons Shape Pos t0 a2 a0) a3_0)
+              end.
+
+Definition rev (Shape : Type) (Pos : Shape -> Type) {t0 : Type} (a0
+    : Free Shape Pos (List Shape Pos t0)) (a1 : Free Shape Pos (List Shape Pos t0))
+   : Free Shape Pos (List Shape Pos t0) :=
+  a1 >>= (fun (a1_0 : List Shape Pos t0) => @rev_0 Shape Pos t0 a0 a1_0).
+
+Definition reverse (Shape : Type) (Pos : Shape -> Type) {a : Type} (xs
+    : Free Shape Pos (List Shape Pos a))
+   : Free Shape Pos (List Shape Pos a) :=
+  @rev Shape Pos a (@Nil Shape Pos a) xs.
+
+Definition prop_rev_is_rev_inv (Shape : Type) (Pos : Shape -> Type) {a : Type}
+  (xs : Free Shape Pos (List Shape Pos a))
+   : Free Shape Pos (Property Shape Pos) :=
+  @eqProp Shape Pos (List Shape Pos a) (@reverse Shape Pos a (@reverse Shape Pos a
+                                                              xs)) xs.
+
+Definition pred (Shape : Type) (Pos : Shape -> Type) (a12
+    : Free Shape Pos (Peano Shape Pos))
+   : Free Shape Pos (Peano Shape Pos) :=
+  a12 >>=
+  (fun a12_0 => match a12_0 with | zero => Zero Shape Pos | s a13 => a13 end).
+
+Section section_map_0.
+(* Constant arguments for map *)
+Variable Shape : Type.
+Variable Pos : Shape -> Type.
+Variable a_0 b_0 : Type.
+Variable a6_0 : Free Shape Pos (Free Shape Pos a_0 -> Free Shape Pos b_0).
+(* Helper functions for map *)
+Fixpoint map_1 (a7 : List Shape Pos a_0) {struct a7} : Free Shape Pos (List
+                                                             Shape Pos b_0)
+           := match a7 with
+              | nil => @Nil Shape Pos b_0
+              | cons a8 a9 =>
+                  @Cons Shape Pos b_0 (a6_0 >>= (fun a6_1 => a6_1 a8)) (a9 >>=
+                                       (fun (a9_0 : List Shape Pos a_0) => map_1 a9_0))
+              end.
+(* Main functions for map *)
+Definition map_0 (a7 : Free Shape Pos (List Shape Pos a_0))
+   : Free Shape Pos (List Shape Pos b_0) :=
+  a7 >>= (fun (a7_0 : List Shape Pos a_0) => map_1 a7_0).
+End section_map_0.
+
+Definition map (Shape : Type) (Pos : Shape -> Type) {a b : Type} (a6
+    : Free Shape Pos (Free Shape Pos a -> Free Shape Pos b)) (a7
+    : Free Shape Pos (List Shape Pos a))
+   : Free Shape Pos (List Shape Pos b) :=
+  map_0 Shape Pos a b a6 a7.
+
+Definition id (Shape : Type) (Pos : Shape -> Type) {a : Type} (a0
+    : Free Shape Pos a)
+   : Free Shape Pos a :=
+  a0.
+
+Section section_foldPeano_0.
+(* Constant arguments for foldPeano *)
+Variable Shape : Type.
+Variable Pos : Shape -> Type.
+Variable a_0 : Type.
+Variable a16_0 : Free Shape Pos a_0.
+Variable a15_0 : Free Shape Pos (Free Shape Pos a_0 -> Free Shape Pos a_0).
+(* Helper functions for foldPeano *)
+Fixpoint foldPeano_1 (a17 : Peano Shape Pos) {struct a17} : Free Shape Pos a_0
+           := match a17 with
+              | zero => a16_0
+              | s a18 =>
+                  a15_0 >>=
+                  (fun a15_1 =>
+                     a15_1 (a18 >>= (fun (a18_0 : Peano Shape Pos) => foldPeano_1 a18_0)))
+              end.
+(* Main functions for foldPeano *)
+Definition foldPeano_0 (a17 : Free Shape Pos (Peano Shape Pos))
+   : Free Shape Pos a_0 :=
+  a17 >>= (fun (a17_0 : Peano Shape Pos) => foldPeano_1 a17_0).
+End section_foldPeano_0.
+
+Definition foldPeano (Shape : Type) (Pos : Shape -> Type) {a : Type} (a15
+    : Free Shape Pos (Free Shape Pos a -> Free Shape Pos a)) (a16
+    : Free Shape Pos a) (a17 : Free Shape Pos (Peano Shape Pos))
+   : Free Shape Pos a :=
+  foldPeano_0 Shape Pos a a16 a15 a17.
+
+Definition minus (Shape : Type) (Pos : Shape -> Type) (x_0
+    : Free Shape Pos (Peano Shape Pos)) (x_1 : Free Shape Pos (Peano Shape Pos))
+   : Free Shape Pos (Peano Shape Pos) :=
+  @foldPeano Shape Pos (Peano Shape Pos) (pure (fun x_2 => pred Shape Pos x_2))
+                                         x_0 x_1.
+
+Definition plus (Shape : Type) (Pos : Shape -> Type) (x_0
+    : Free Shape Pos (Peano Shape Pos)) (x_1 : Free Shape Pos (Peano Shape Pos))
+   : Free Shape Pos (Peano Shape Pos) :=
+  @foldPeano Shape Pos (Peano Shape Pos) (pure (fun x_2 => S Shape Pos x_2)) x_0
+                                         x_1.
+
+Definition comp (Shape : Type) (Pos : Shape -> Type) {b c a : Type} (g
+    : Free Shape Pos (Free Shape Pos b -> Free Shape Pos c)) (f
+    : Free Shape Pos (Free Shape Pos a -> Free Shape Pos b)) (a0
+    : Free Shape Pos a)
+   : Free Shape Pos c :=
+  g >>= (fun g_0 => g_0 (f >>= (fun f_0 => f_0 a0))).

From 5569e2f115930b36ae5b05ec0c3c903db93df65c Mon Sep 17 00:00:00 2001
From: jo-hanna1997 <stu203549@mail.uni-kiel.de>
Date: Tue, 23 Jun 2020 11:18:50 +0200
Subject: [PATCH 03/16] Introduce proof outline in non-monadic setting for
 reverse is involution

---
 .../CaseStudyMorallyCorrect/Output/Proofs.v   | 74 +++++++++++++++++++
 1 file changed, 74 insertions(+)
 create mode 100644 example/CaseStudyMorallyCorrect/Output/Proofs.v

diff --git a/example/CaseStudyMorallyCorrect/Output/Proofs.v b/example/CaseStudyMorallyCorrect/Output/Proofs.v
new file mode 100644
index 00000000..69482c3d
--- /dev/null
+++ b/example/CaseStudyMorallyCorrect/Output/Proofs.v
@@ -0,0 +1,74 @@
+From Base Require Import Test.QuickCheck.
+From Base Require Import Free.Instance.Identity.
+From Base Require Import Free.
+From Base Require Import Prelude.List.
+From Generated Require Import FastLooseBasic.
+
+Inductive List (A :Type) : Type :=
+|nil : List A
+|cons : A -> List A -> List A.
+
+Arguments nil {_}.
+Arguments cons {_} _ _.
+
+Section rev.
+
+Variable A : Type.
+
+Fixpoint rev (acc : List A) (xs : List A) : List A :=
+  match xs with
+  | nil => acc
+  | cons x xs' => rev (cons x acc) xs'
+  end.
+
+Definition reverse (xs : List A) : List A :=
+ rev nil xs.
+
+Fixpoint append (xs : List A) (ys : List A) : List A :=
+match xs with
+| nil => ys
+| cons x xs' => cons x (append xs' ys)
+end.
+
+Fixpoint reverse2 (xs : List A) : List A :=
+match xs with
+| nil => nil
+| cons x xs => append (reverse2 xs) (cons x nil)
+end.
+
+
+Theorem app_nil: forall (xs : List A), append xs nil = xs.
+Proof.
+Admitted.
+
+Theorem rev_append: forall (xs : List A) (ys : List A),
+rev ys xs = append (reverse xs) ys.
+Proof.
+intros xs.
+induction xs.
+- reflexivity.
+- simpl.
+  intros. unfold reverse. simpl. rewrite IHxs. rewrite IHxs.
+Admitted.
+
+
+Theorem reverse2_reverse1: forall (xs : List A), reverse2 xs = reverse xs.
+Proof.
+intros.
+induction xs.
+- reflexivity.
+- simpl. unfold reverse. simpl. rewrite rev_append. rewrite IHxs. reflexivity.
+Qed.
+
+
+End rev.
+
+Theorem rev_inv_rev: quickCheck (@prop_rev_is_rev_inv Identity.Shape Identity.Pos).
+Proof.
+  simpl.
+  intros A totalList.
+  induction totalList as [ xs | [] ] using Free_Ind.
+  - induction xs as [ | x [xs' | []]] using List_Ind.
+    + reflexivity.
+    + simplify H as H'. simpl.
+Qed.
\ No newline at end of file

From b2e63991e387f0dc8be9874fd75dd8a01111b063 Mon Sep 17 00:00:00 2001
From: Johanna <jo-hanna_menzel@live.de>
Date: Tue, 23 Jun 2020 19:33:29 +0200
Subject: [PATCH 04/16] Start transfering reverse_is_reverseNaive proof into
 monadic setting

---
 .../Output/AppendProofs.v                     |  41 ++++++
 .../Output/FastLooseBasic.json                |  29 +++-
 .../Output/FastLooseBasic.v                   | 134 ++++++++++++------
 .../CaseStudyMorallyCorrect/Output/Proofs.v   |  67 +++++++--
 4 files changed, 219 insertions(+), 52 deletions(-)
 create mode 100644 example/CaseStudyMorallyCorrect/Output/AppendProofs.v

diff --git a/example/CaseStudyMorallyCorrect/Output/AppendProofs.v b/example/CaseStudyMorallyCorrect/Output/AppendProofs.v
new file mode 100644
index 00000000..ad7b7d3e
--- /dev/null
+++ b/example/CaseStudyMorallyCorrect/Output/AppendProofs.v
@@ -0,0 +1,41 @@
+From Base Require Import Free.
+From Base Require Import Prelude.List.
+From Generated Require Import FastLooseBasic.
+Require Import Coq.Logic.FunctionalExtensionality.
+
+Set Implicit Arguments.
+
+Arguments append {_} {_} {_} _ _.
+
+Lemma append_assoc' : forall (Shape : Type) (Pos : Shape -> Type) (A : Type)
+  (xs : List Shape Pos A) (fys fzs : Free Shape Pos (List Shape Pos A)),
+  append (pure xs) (append fys fzs) = append (append (pure xs) fys) fzs.
+Proof.
+  intros.
+  induction xs as [| fx fxs IH] using List_Ind.
+  - reflexivity.
+  - induction fxs as [xs | s pf IHpf] using Free_Ind.
+    + simpl. f_equal. simplify H as IH'. simpl in IH'. apply IH'.
+    + simpl. do 2 apply f_equal. extensionality x.
+Admitted. 
+
+Lemma append_assoc : forall (Shape : Type) (Pos : Shape -> Type) (A : Type)
+  (fxs fys fzs : Free Shape Pos (List Shape Pos A)),
+  append fxs (append fys fzs) = append (append fxs fys) fzs.
+Proof.
+  intros.
+  induction fxs using Free_Ind.
+  - apply append_assoc'.
+  - simpl. f_equal. extensionality p.
+    apply H.
+Qed.
+
+Lemma append_nil : forall (Shape : Type) (Pos : Shape -> Type) (A : Type)
+  (fxs : Free Shape Pos (List Shape Pos A)),
+  append fxs (Nil Shape Pos) = fxs.
+Proof.
+Admitted.
+
+
+
+
diff --git a/example/CaseStudyMorallyCorrect/Output/FastLooseBasic.json b/example/CaseStudyMorallyCorrect/Output/FastLooseBasic.json
index 3594889d..f269c4c4 100644
--- a/example/CaseStudyMorallyCorrect/Output/FastLooseBasic.json
+++ b/example/CaseStudyMorallyCorrect/Output/FastLooseBasic.json
@@ -4,6 +4,7 @@
     "exported-values": [
         "FastLooseBasic.S",
         "FastLooseBasic.Zero",
+        "FastLooseBasic.append",
         "FastLooseBasic.comp",
         "FastLooseBasic.foldPeano",
         "FastLooseBasic.id",
@@ -12,8 +13,10 @@
         "FastLooseBasic.plus",
         "FastLooseBasic.pred",
         "FastLooseBasic.prop_rev_is_rev_inv",
+        "FastLooseBasic.prop_reverse_is_reverseNaive",
         "FastLooseBasic.rev",
-        "FastLooseBasic.reverse"
+        "FastLooseBasic.reverse",
+        "FastLooseBasic.reverseNaive"
     ],
     "module-name": "FastLooseBasic",
     "exported-types": [
@@ -136,6 +139,14 @@
     ],
     "version": 3,
     "functions": [
+        {
+            "arity": 2,
+            "haskell-type": "Prelude.([]) a -> Prelude.([]) a -> Prelude.([]) a",
+            "coq-name": "append",
+            "needs-free-args": true,
+            "partial": false,
+            "haskell-name": "FastLooseBasic.append"
+        },
         {
             "arity": 3,
             "haskell-type": "(b -> c) -> (a -> b) -> a -> c",
@@ -200,6 +211,14 @@
             "partial": false,
             "haskell-name": "FastLooseBasic.prop_rev_is_rev_inv"
         },
+        {
+            "arity": 1,
+            "haskell-type": "Prelude.([]) a -> Test.QuickCheck.Property",
+            "coq-name": "prop_reverse_is_reverseNaive",
+            "needs-free-args": true,
+            "partial": false,
+            "haskell-name": "FastLooseBasic.prop_reverse_is_reverseNaive"
+        },
         {
             "arity": 2,
             "haskell-type": "Prelude.([]) t0 -> Prelude.([]) t0 -> Prelude.([]) t0",
@@ -216,6 +235,14 @@
             "partial": false,
             "haskell-name": "FastLooseBasic.reverse"
         },
+        {
+            "arity": 1,
+            "haskell-type": "Prelude.([]) a -> Prelude.([]) a",
+            "coq-name": "reverseNaive",
+            "needs-free-args": true,
+            "partial": false,
+            "haskell-name": "FastLooseBasic.reverseNaive"
+        },
         {
             "arity": 1,
             "haskell-type": "Prelude.Integer -> Prelude.Integer -> Prelude.Integer",
diff --git a/example/CaseStudyMorallyCorrect/Output/FastLooseBasic.v b/example/CaseStudyMorallyCorrect/Output/FastLooseBasic.v
index beee1822..a2c2b43b 100644
--- a/example/CaseStudyMorallyCorrect/Output/FastLooseBasic.v
+++ b/example/CaseStudyMorallyCorrect/Output/FastLooseBasic.v
@@ -31,26 +31,27 @@ Definition S (Shape : Type) (Pos : Shape -> Type) (x_0
 
 (* Helper functions for rev *)
 
-Fixpoint rev_0 (Shape : Type) (Pos : Shape -> Type) {t0 : Type} (a0
-                 : Free Shape Pos (List Shape Pos t0)) (a1 : List Shape Pos t0) {struct a1}
+Fixpoint rev_0 (Shape : Type) (Pos : Shape -> Type) {t0 : Type} (a11
+                 : List Shape Pos t0) (a12 : Free Shape Pos (List Shape Pos t0)) {struct a11}
            : Free Shape Pos (List Shape Pos t0)
-           := match a1 with
-              | nil => a0
-              | cons a2 a3 =>
-                  a3 >>=
-                  (fun (a3_0 : List Shape Pos t0) =>
-                     @rev_0 Shape Pos t0 (@Cons Shape Pos t0 a2 a0) a3_0)
+           := match a11 with
+              | nil => a12
+              | cons a13 a14 =>
+                  a14 >>=
+                  (fun (a14_0 : List Shape Pos t0) =>
+                     @rev_0 Shape Pos t0 a14_0 (@Cons Shape Pos t0 a13 a12))
               end.
 
-Definition rev (Shape : Type) (Pos : Shape -> Type) {t0 : Type} (a0
-    : Free Shape Pos (List Shape Pos t0)) (a1 : Free Shape Pos (List Shape Pos t0))
+Definition rev (Shape : Type) (Pos : Shape -> Type) {t0 : Type} (a11
+    : Free Shape Pos (List Shape Pos t0)) (a12
+    : Free Shape Pos (List Shape Pos t0))
    : Free Shape Pos (List Shape Pos t0) :=
-  a1 >>= (fun (a1_0 : List Shape Pos t0) => @rev_0 Shape Pos t0 a0 a1_0).
+  a11 >>= (fun (a11_0 : List Shape Pos t0) => @rev_0 Shape Pos t0 a11_0 a12).
 
 Definition reverse (Shape : Type) (Pos : Shape -> Type) {a : Type} (xs
     : Free Shape Pos (List Shape Pos a))
    : Free Shape Pos (List Shape Pos a) :=
-  @rev Shape Pos a (@Nil Shape Pos a) xs.
+  @rev Shape Pos a xs (@Nil Shape Pos a).
 
 Definition prop_rev_is_rev_inv (Shape : Type) (Pos : Shape -> Type) {a : Type}
   (xs : Free Shape Pos (List Shape Pos a))
@@ -58,38 +59,38 @@ Definition prop_rev_is_rev_inv (Shape : Type) (Pos : Shape -> Type) {a : Type}
   @eqProp Shape Pos (List Shape Pos a) (@reverse Shape Pos a (@reverse Shape Pos a
                                                               xs)) xs.
 
-Definition pred (Shape : Type) (Pos : Shape -> Type) (a12
+Definition pred (Shape : Type) (Pos : Shape -> Type) (a23
     : Free Shape Pos (Peano Shape Pos))
    : Free Shape Pos (Peano Shape Pos) :=
-  a12 >>=
-  (fun a12_0 => match a12_0 with | zero => Zero Shape Pos | s a13 => a13 end).
+  a23 >>=
+  (fun a23_0 => match a23_0 with | zero => Zero Shape Pos | s a24 => a24 end).
 
 Section section_map_0.
 (* Constant arguments for map *)
 Variable Shape : Type.
 Variable Pos : Shape -> Type.
 Variable a_0 b_0 : Type.
-Variable a6_0 : Free Shape Pos (Free Shape Pos a_0 -> Free Shape Pos b_0).
+Variable a17_0 : Free Shape Pos (Free Shape Pos a_0 -> Free Shape Pos b_0).
 (* Helper functions for map *)
-Fixpoint map_1 (a7 : List Shape Pos a_0) {struct a7} : Free Shape Pos (List
-                                                             Shape Pos b_0)
-           := match a7 with
+Fixpoint map_1 (a18 : List Shape Pos a_0) {struct a18} : Free Shape Pos (List
+                                                               Shape Pos b_0)
+           := match a18 with
               | nil => @Nil Shape Pos b_0
-              | cons a8 a9 =>
-                  @Cons Shape Pos b_0 (a6_0 >>= (fun a6_1 => a6_1 a8)) (a9 >>=
-                                       (fun (a9_0 : List Shape Pos a_0) => map_1 a9_0))
+              | cons a19 a20 =>
+                  @Cons Shape Pos b_0 (a17_0 >>= (fun a17_1 => a17_1 a19)) (a20 >>=
+                                       (fun (a20_0 : List Shape Pos a_0) => map_1 a20_0))
               end.
 (* Main functions for map *)
-Definition map_0 (a7 : Free Shape Pos (List Shape Pos a_0))
+Definition map_0 (a18 : Free Shape Pos (List Shape Pos a_0))
    : Free Shape Pos (List Shape Pos b_0) :=
-  a7 >>= (fun (a7_0 : List Shape Pos a_0) => map_1 a7_0).
+  a18 >>= (fun (a18_0 : List Shape Pos a_0) => map_1 a18_0).
 End section_map_0.
 
-Definition map (Shape : Type) (Pos : Shape -> Type) {a b : Type} (a6
-    : Free Shape Pos (Free Shape Pos a -> Free Shape Pos b)) (a7
+Definition map (Shape : Type) (Pos : Shape -> Type) {a b : Type} (a17
+    : Free Shape Pos (Free Shape Pos a -> Free Shape Pos b)) (a18
     : Free Shape Pos (List Shape Pos a))
    : Free Shape Pos (List Shape Pos b) :=
-  map_0 Shape Pos a b a6 a7.
+  map_0 Shape Pos a b a17 a18.
 
 Definition id (Shape : Type) (Pos : Shape -> Type) {a : Type} (a0
     : Free Shape Pos a)
@@ -101,28 +102,28 @@ Section section_foldPeano_0.
 Variable Shape : Type.
 Variable Pos : Shape -> Type.
 Variable a_0 : Type.
-Variable a16_0 : Free Shape Pos a_0.
-Variable a15_0 : Free Shape Pos (Free Shape Pos a_0 -> Free Shape Pos a_0).
+Variable a27_0 : Free Shape Pos a_0.
+Variable a26_0 : Free Shape Pos (Free Shape Pos a_0 -> Free Shape Pos a_0).
 (* Helper functions for foldPeano *)
-Fixpoint foldPeano_1 (a17 : Peano Shape Pos) {struct a17} : Free Shape Pos a_0
-           := match a17 with
-              | zero => a16_0
-              | s a18 =>
-                  a15_0 >>=
-                  (fun a15_1 =>
-                     a15_1 (a18 >>= (fun (a18_0 : Peano Shape Pos) => foldPeano_1 a18_0)))
+Fixpoint foldPeano_1 (a28 : Peano Shape Pos) {struct a28} : Free Shape Pos a_0
+           := match a28 with
+              | zero => a27_0
+              | s a29 =>
+                  a26_0 >>=
+                  (fun a26_1 =>
+                     a26_1 (a29 >>= (fun (a29_0 : Peano Shape Pos) => foldPeano_1 a29_0)))
               end.
 (* Main functions for foldPeano *)
-Definition foldPeano_0 (a17 : Free Shape Pos (Peano Shape Pos))
+Definition foldPeano_0 (a28 : Free Shape Pos (Peano Shape Pos))
    : Free Shape Pos a_0 :=
-  a17 >>= (fun (a17_0 : Peano Shape Pos) => foldPeano_1 a17_0).
+  a28 >>= (fun (a28_0 : Peano Shape Pos) => foldPeano_1 a28_0).
 End section_foldPeano_0.
 
-Definition foldPeano (Shape : Type) (Pos : Shape -> Type) {a : Type} (a15
-    : Free Shape Pos (Free Shape Pos a -> Free Shape Pos a)) (a16
-    : Free Shape Pos a) (a17 : Free Shape Pos (Peano Shape Pos))
+Definition foldPeano (Shape : Type) (Pos : Shape -> Type) {a : Type} (a26
+    : Free Shape Pos (Free Shape Pos a -> Free Shape Pos a)) (a27
+    : Free Shape Pos a) (a28 : Free Shape Pos (Peano Shape Pos))
    : Free Shape Pos a :=
-  foldPeano_0 Shape Pos a a16 a15 a17.
+  foldPeano_0 Shape Pos a a27 a26 a28.
 
 Definition minus (Shape : Type) (Pos : Shape -> Type) (x_0
     : Free Shape Pos (Peano Shape Pos)) (x_1 : Free Shape Pos (Peano Shape Pos))
@@ -142,3 +143,52 @@ Definition comp (Shape : Type) (Pos : Shape -> Type) {b c a : Type} (g
     : Free Shape Pos a)
    : Free Shape Pos c :=
   g >>= (fun g_0 => g_0 (f >>= (fun f_0 => f_0 a0))).
+
+Section section_append_0.
+(* Constant arguments for append *)
+Variable Shape : Type.
+Variable Pos : Shape -> Type.
+Variable a_0 : Type.
+Variable a1_0 : Free Shape Pos (List Shape Pos a_0).
+(* Helper functions for append *)
+Fixpoint append_1 (a0 : List Shape Pos a_0) {struct a0} : Free Shape Pos (List
+                                                                Shape Pos a_0)
+           := match a0 with
+              | nil => a1_0
+              | cons a2 a3 =>
+                  @Cons Shape Pos a_0 a2 (a3 >>=
+                                       (fun (a3_0 : List Shape Pos a_0) => append_1 a3_0))
+              end.
+(* Main functions for append *)
+Definition append_0 (a0 : Free Shape Pos (List Shape Pos a_0))
+   : Free Shape Pos (List Shape Pos a_0) :=
+  a0 >>= (fun (a0_0 : List Shape Pos a_0) => append_1 a0_0).
+End section_append_0.
+
+Definition append (Shape : Type) (Pos : Shape -> Type) {a : Type} (a0
+    : Free Shape Pos (List Shape Pos a)) (a1 : Free Shape Pos (List Shape Pos a))
+   : Free Shape Pos (List Shape Pos a) :=
+  append_0 Shape Pos a a1 a0.
+
+(* Helper functions for reverseNaive *)
+
+Fixpoint reverseNaive_0 (Shape : Type) (Pos : Shape -> Type) {a : Type} (a6
+                          : List Shape Pos a) {struct a6} : Free Shape Pos (List Shape Pos a)
+           := match a6 with
+              | nil => @Nil Shape Pos a
+              | cons a7 a8 =>
+                  @append Shape Pos a (a8 >>=
+                                       (fun (a8_0 : List Shape Pos a) => @reverseNaive_0 Shape Pos a a8_0)) (@Cons
+                                       Shape Pos a a7 (@Nil Shape Pos a))
+              end.
+
+Definition reverseNaive (Shape : Type) (Pos : Shape -> Type) {a : Type} (a6
+    : Free Shape Pos (List Shape Pos a))
+   : Free Shape Pos (List Shape Pos a) :=
+  a6 >>= (fun (a6_0 : List Shape Pos a) => @reverseNaive_0 Shape Pos a a6_0).
+
+Definition prop_reverse_is_reverseNaive (Shape : Type) (Pos : Shape -> Type) {a
+   : Type} (xs : Free Shape Pos (List Shape Pos a))
+   : Free Shape Pos (Property Shape Pos) :=
+  @eqProp Shape Pos (List Shape Pos a) (@reverse Shape Pos a xs) (@reverseNaive
+                                        Shape Pos a xs).
diff --git a/example/CaseStudyMorallyCorrect/Output/Proofs.v b/example/CaseStudyMorallyCorrect/Output/Proofs.v
index 69482c3d..ce5eb497 100644
--- a/example/CaseStudyMorallyCorrect/Output/Proofs.v
+++ b/example/CaseStudyMorallyCorrect/Output/Proofs.v
@@ -3,15 +3,18 @@ From Base Require Import Free.Instance.Identity.
 From Base Require Import Free.
 From Base Require Import Prelude.List.
 From Generated Require Import FastLooseBasic.
+From Generated Require Import AppendProofs.
+Require Import Coq.Logic.FunctionalExtensionality.
 
-Inductive List (A :Type) : Type :=
-|nil : List A
-|cons : A -> List A -> List A.
+Set Implicit Arguments.
 
-Arguments nil {_}.
-Arguments cons {_} _ _.
+Arguments rev {_} {_} {_} _ _.
+Arguments reverse {_} {_} {_} _ .
+Arguments reverseNaive {_} {_} {_} _ .
+Arguments append {_} {_} {_} _ _.
 
-Section rev.
+
+(*Section rev.
 
 Variable A : Type.
 
@@ -42,7 +45,7 @@ Proof.
 Admitted.
 
 Theorem rev_append: forall (xs : List A) (ys : List A),
-rev ys xs = append (reverse xs) ys.
+rev xs acc = append (reverse xs) ys.
 Proof.
 intros xs.
 induction xs.
@@ -61,7 +64,51 @@ induction xs.
 Qed.
 
 
-End rev.
+End rev.*)
+
+Section reverseIsReverseNaive.
+
+Lemma rev_acc_and_rest_list_connection': forall (Shape : Type) (Pos : Shape -> Type) (A : Type)
+  (xs : List Shape Pos A) (facc : Free Shape Pos (List Shape Pos A)),  
+  rev (pure xs) facc = append (reverse (pure xs)) facc.
+Proof.
+  intros Shape Pos A xs.
+  induction xs as [ | x fxs' ] using List_Ind; intros.
+  - reflexivity.
+  - induction fxs' as [ xs' | sh pos ] using Free_Ind.
+    + simplify H as IHxs'. simpl. simpl in IHxs'. rewrite IHxs'. rewrite IHxs'. 
+      assert (H : rev_0 Shape Pos xs' (Cons Shape Pos x (Nil Shape Pos)) = 
+           append (rev_0 Shape Pos xs' (Nil Shape Pos)) (Cons Shape Pos x (Nil Shape Pos))).
+      {rewrite IHxs'. reflexivity. }
+      rewrite H. rewrite append_nil. rewrite <- append_assoc. reflexivity.
+    + 
+
+Lemma rev_acc_and_rest_list_connection: forall (Shape : Type) (Pos : Shape -> Type) (A : Type)
+  (fxs : Free Shape Pos (List Shape Pos A)) (facc : Free Shape Pos (List Shape Pos A)),
+  rev fxs facc = append (reverse fxs) facc.
+Proof.
+  intros Shape Pos A fxs facc.
+  induction fxs as [ xs | sh pos ] using Free_Ind.
+  - 
+
+
+Lemma reverse_is_reverseNaive': forall (Shape : Type) (Pos : Shape -> Type) (A : Type)
+  (xs : List Shape Pos A),
+  reverse Shape Pos (pure xs) = reverseNaive Shape Pos (pure xs).
+Proof.
+  intros Shape Pos A xs.
+  induction xs as [ | x fxs' ] using List_Ind.
+  - reflexivity.
+  - induction fxs' as [ xs' | sh pos ] using Free_Ind.
+    + simplify H as IHxs'. unfold reverse. 
+
+
+Theorem reverse_is_reverseNaive: quickCheck prop_reverse_is_reverseNaive.
+Proof.
+  simpl.
+  intros Shape Pos A fxs.
+  induction fxs as [ xs | sh pos ] using Free_Ind.
+  - 
 
 Theorem rev_inv_rev: quickCheck (@prop_rev_is_rev_inv Identity.Shape Identity.Pos).
 Proof.
@@ -71,4 +118,6 @@ Proof.
   - induction xs as [ | x [xs' | []]] using List_Ind.
     + reflexivity.
     + simplify H as H'. simpl.
-Qed.
\ No newline at end of file
+Qed.
+
+Section reverseIsReverseNaive.
\ No newline at end of file

From 6d1679dc9c166dd2b0e0fccf14182bf0c84cc5f9 Mon Sep 17 00:00:00 2001
From: Johanna <jo-hanna_menzel@live.de>
Date: Fri, 26 Jun 2020 10:56:46 +0200
Subject: [PATCH 05/16] Complete main part of proof reverse_is_reverseNaive

---
 .../FastAndLooseReasoning.hs                  | 17 +++-
 .../CaseStudyMorallyCorrect/Output/Proofs.v   | 79 +++++--------------
 .../CaseStudyMorallyCorrect/Output/Simplify.v | 47 +++++++++++
 3 files changed, 80 insertions(+), 63 deletions(-)
 create mode 100644 example/CaseStudyMorallyCorrect/Output/Simplify.v

diff --git a/example/CaseStudyMorallyCorrect/FastAndLooseReasoning.hs b/example/CaseStudyMorallyCorrect/FastAndLooseReasoning.hs
index 09f7bf61..1d059448 100644
--- a/example/CaseStudyMorallyCorrect/FastAndLooseReasoning.hs
+++ b/example/CaseStudyMorallyCorrect/FastAndLooseReasoning.hs
@@ -4,11 +4,19 @@ import           Test.QuickCheck
 
 data Peano = Zero | S Peano
 
+append :: [a] -> [a] -> [a]
+append []       ys = ys
+append (x : xs) ys = x : (append xs ys)
+
+reverseNaive :: [a] -> [a]
+reverseNaive []       = []
+reverseNaive (x : xs) = append (reverseNaive xs) [x]
+
 reverse :: [a] -> [a]
-reverse xs = rev [] xs
+reverse xs = rev xs []
 
-rev acc []       = acc
-rev acc (x : xs) = rev (x : acc) xs
+rev []       acc = acc
+rev (x : xs) acc = rev xs (x : acc)
 
 map :: (a -> b) -> [a] -> [b]
 map f []       = []
@@ -34,5 +42,8 @@ foldPeano :: (a -> a) -> a -> Peano -> a
 foldPeano f a Zero  = a
 foldPeano f a (S n) = f (foldPeano f a n)
 
+prop_reverse_is_reverseNaive :: [a] -> Property
+prop_reverse_is_reverseNaive xs = reverse xs === reverseNaive xs
+
 prop_rev_is_rev_inv :: [a] -> Property
 prop_rev_is_rev_inv xs = reverse (reverse xs) === xs
diff --git a/example/CaseStudyMorallyCorrect/Output/Proofs.v b/example/CaseStudyMorallyCorrect/Output/Proofs.v
index ce5eb497..b72cf997 100644
--- a/example/CaseStudyMorallyCorrect/Output/Proofs.v
+++ b/example/CaseStudyMorallyCorrect/Output/Proofs.v
@@ -4,6 +4,7 @@ From Base Require Import Free.
 From Base Require Import Prelude.List.
 From Generated Require Import FastLooseBasic.
 From Generated Require Import AppendProofs.
+From Generated Require Import Simplify.
 Require Import Coq.Logic.FunctionalExtensionality.
 
 Set Implicit Arguments.
@@ -13,59 +14,6 @@ Arguments reverse {_} {_} {_} _ .
 Arguments reverseNaive {_} {_} {_} _ .
 Arguments append {_} {_} {_} _ _.
 
-
-(*Section rev.
-
-Variable A : Type.
-
-Fixpoint rev (acc : List A) (xs : List A) : List A :=
-  match xs with
-  | nil => acc
-  | cons x xs' => rev (cons x acc) xs'
-  end.
-
-Definition reverse (xs : List A) : List A :=
- rev nil xs.
-
-Fixpoint append (xs : List A) (ys : List A) : List A :=
-match xs with
-| nil => ys
-| cons x xs' => cons x (append xs' ys)
-end.
-
-Fixpoint reverse2 (xs : List A) : List A :=
-match xs with
-| nil => nil
-| cons x xs => append (reverse2 xs) (cons x nil)
-end.
-
-
-Theorem app_nil: forall (xs : List A), append xs nil = xs.
-Proof.
-Admitted.
-
-Theorem rev_append: forall (xs : List A) (ys : List A),
-rev xs acc = append (reverse xs) ys.
-Proof.
-intros xs.
-induction xs.
-- reflexivity.
-- simpl.
-  intros. unfold reverse. simpl. rewrite IHxs. rewrite IHxs.
-Admitted.
-
-
-Theorem reverse2_reverse1: forall (xs : List A), reverse2 xs = reverse xs.
-Proof.
-intros.
-induction xs.
-- reflexivity.
-- simpl. unfold reverse. simpl. rewrite rev_append. rewrite IHxs. reflexivity.
-Qed.
-
-
-End rev.*)
-
 Section reverseIsReverseNaive.
 
 Lemma rev_acc_and_rest_list_connection': forall (Shape : Type) (Pos : Shape -> Type) (A : Type)
@@ -76,12 +24,13 @@ Proof.
   induction xs as [ | x fxs' ] using List_Ind; intros.
   - reflexivity.
   - induction fxs' as [ xs' | sh pos ] using Free_Ind.
-    + simplify H as IHxs'. simpl. simpl in IHxs'. rewrite IHxs'. rewrite IHxs'. 
+    + simplify2 H as IHxs'. simpl. simpl in IHxs'. rewrite IHxs'. rewrite IHxs'. 
       assert (H : rev_0 Shape Pos xs' (Cons Shape Pos x (Nil Shape Pos)) = 
            append (rev_0 Shape Pos xs' (Nil Shape Pos)) (Cons Shape Pos x (Nil Shape Pos))).
       {rewrite IHxs'. reflexivity. }
       rewrite H. rewrite append_nil. rewrite <- append_assoc. reflexivity.
-    + 
+    + simpl. f_equal. extensionality x0. simplify2 H0 as H0'. apply H0'.
+Qed.
 
 Lemma rev_acc_and_rest_list_connection: forall (Shape : Type) (Pos : Shape -> Type) (A : Type)
   (fxs : Free Shape Pos (List Shape Pos A)) (facc : Free Shape Pos (List Shape Pos A)),
@@ -89,18 +38,25 @@ Lemma rev_acc_and_rest_list_connection: forall (Shape : Type) (Pos : Shape -> Ty
 Proof.
   intros Shape Pos A fxs facc.
   induction fxs as [ xs | sh pos ] using Free_Ind.
-  - 
-
+  - apply rev_acc_and_rest_list_connection'.
+  - simpl. f_equal. extensionality x. apply H.
+Qed.
 
 Lemma reverse_is_reverseNaive': forall (Shape : Type) (Pos : Shape -> Type) (A : Type)
   (xs : List Shape Pos A),
-  reverse Shape Pos (pure xs) = reverseNaive Shape Pos (pure xs).
+  reverse (pure xs) = reverseNaive (pure xs).
 Proof.
   intros Shape Pos A xs.
   induction xs as [ | x fxs' ] using List_Ind.
   - reflexivity.
   - induction fxs' as [ xs' | sh pos ] using Free_Ind.
-    + simplify H as IHxs'. unfold reverse. 
+    + simplify H as IHxs'. simpl reverseNaive. simpl reverse.
+      assert  (H : rev_0 Shape Pos xs' (Cons Shape Pos x (Nil Shape Pos)) = 
+                   rev (pure xs') (Cons Shape Pos x (Nil Shape Pos))).
+      {reflexivity. }
+      rewrite H. rewrite rev_acc_and_rest_list_connection. rewrite IHxs'. reflexivity.
+    + simpl. f_equal. extensionality x0. simplify2 H0 as H0'. apply H0'.
+Qed.
 
 
 Theorem reverse_is_reverseNaive: quickCheck prop_reverse_is_reverseNaive.
@@ -108,7 +64,9 @@ Proof.
   simpl.
   intros Shape Pos A fxs.
   induction fxs as [ xs | sh pos ] using Free_Ind.
-  - 
+  - apply reverse_is_reverseNaive'.
+  - simpl. f_equal. extensionality x. apply H.
+Qed.
 
 Theorem rev_inv_rev: quickCheck (@prop_rev_is_rev_inv Identity.Shape Identity.Pos).
 Proof.
@@ -118,6 +76,7 @@ Proof.
   - induction xs as [ | x [xs' | []]] using List_Ind.
     + reflexivity.
     + simplify H as H'. simpl.
+
 Qed.
 
 Section reverseIsReverseNaive.
\ No newline at end of file
diff --git a/example/CaseStudyMorallyCorrect/Output/Simplify.v b/example/CaseStudyMorallyCorrect/Output/Simplify.v
new file mode 100644
index 00000000..d4e715cb
--- /dev/null
+++ b/example/CaseStudyMorallyCorrect/Output/Simplify.v
@@ -0,0 +1,47 @@
+From Base Require Import Free.
+Require Import Coq.Program.Equality.
+
+Ltac typeof s := let T := type of s in T.
+
+Ltac checkHypothesisIdent ident :=
+  first [ rename ident into HypTmp; rename HypTmp into ident
+        | fail 1 "No such hypothesis" ident ].
+
+Ltac checkFreshIdent ident :=
+  first [ rename ident into HypTmp; rename HypTmp into ident;
+          fail 1 ident "is already used"
+         | idtac ].
+
+Ltac simplifyInductionHypothesis2 ident1 ident2 :=
+  match goal with
+  | [ H0 : ForFree ?Shape ?Pos ?A ?P (impure ?s ?pf) |- _ ] =>
+    dependent destruction H0; try (rename ident2 into Htmp);
+    match goal with
+    | [ H1 : forall p, ForFree ?Shape ?Pos ?A _ (?pf p)
+      , H0 : forall p, ForFree ?Shape ?Pos ?A _ (?pf p) -> _ = _
+      , p : ?Pos ?s |- _ ] =>
+      first [ injection (H0 p (H1 p)) as ident2
+            | specialize (H0 p (H1 p)) as ident2];
+      clear H1; clear H0;
+      try (rename Htmp into ident2)
+    end
+  end.
+
+Ltac searchForInducionHypothesis ident1 ident2 :=
+  checkHypothesisIdent ident1;
+  checkFreshIdent ident2;
+  match typeof ident1 with
+  | context [?s] =>
+    match s with
+    | ForFree ?Shape ?Pos ?A ?P (pure _) =>
+      inversion ident1 as [ Heq ident2 |]; clear ident1; subst
+    | ForFree ?Shape ?Pos ?A ?P (impure ?s ?pf) =>
+      simplifyInductionHypothesis2 ident1 ident2
+    | forall (p : ?Pos ?s), ForFree ?Shape ?Pos ?A ?P (?pf p) -> _ = _ =>
+      simplifyInductionHypothesis2 ident1 ident2
+    | _ => fail 1 "The tactic cannot be applied to the hypothesis" ident1
+    end
+  end.
+
+Tactic Notation "simplify2" ident(H) "as" ident(IH) :=
+  (searchForInducionHypothesis H IH).

From 736cbfaccff6d5c95917e4b464008d1a2eee6496 Mon Sep 17 00:00:00 2001
From: Johanna <jo-hanna_menzel@live.de>
Date: Fri, 26 Jun 2020 11:02:23 +0200
Subject: [PATCH 06/16] Change wrongly Qed into Admitted

---
 example/CaseStudyMorallyCorrect/Output/Proofs.v | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/example/CaseStudyMorallyCorrect/Output/Proofs.v b/example/CaseStudyMorallyCorrect/Output/Proofs.v
index b72cf997..5c2faec0 100644
--- a/example/CaseStudyMorallyCorrect/Output/Proofs.v
+++ b/example/CaseStudyMorallyCorrect/Output/Proofs.v
@@ -76,7 +76,6 @@ Proof.
   - induction xs as [ | x [xs' | []]] using List_Ind.
     + reflexivity.
     + simplify H as H'. simpl.
-
-Qed.
+Admitted.
 
 Section reverseIsReverseNaive.
\ No newline at end of file

From fd9a8295a849ac3b4b29353df97e2cbc7105b54e Mon Sep 17 00:00:00 2001
From: Johanna <jo-hanna_menzel@live.de>
Date: Mon, 29 Jun 2020 12:19:41 +0200
Subject: [PATCH 07/16] Finish proof reverse_is_involution

---
 .../CaseStudyMorallyCorrect/Output/Proofs.v   | 99 +++++++++++++++----
 1 file changed, 82 insertions(+), 17 deletions(-)

diff --git a/example/CaseStudyMorallyCorrect/Output/Proofs.v b/example/CaseStudyMorallyCorrect/Output/Proofs.v
index 5c2faec0..4986b763 100644
--- a/example/CaseStudyMorallyCorrect/Output/Proofs.v
+++ b/example/CaseStudyMorallyCorrect/Output/Proofs.v
@@ -10,12 +10,23 @@ Require Import Coq.Logic.FunctionalExtensionality.
 Set Implicit Arguments.
 
 Arguments rev {_} {_} {_} _ _.
+Arguments rev_0 {_} {_} {_} _ _.
 Arguments reverse {_} {_} {_} _ .
 Arguments reverseNaive {_} {_} {_} _ .
+Arguments reverseNaive_0 {_} {_} {_} _ .
 Arguments append {_} {_} {_} _ _.
+Arguments Nil {_} {_} {_}.
+Arguments Cons {_} {_} {_} _ _.
 
 Section reverseIsReverseNaive.
 
+Lemma rev_0_rev: forall (Shape : Type) (Pos : Shape -> Type) (A : Type)
+  (xs : List Shape Pos A) (fys : Free Shape Pos (List Shape Pos A)),
+  rev_0 xs fys = rev (pure xs) fys.
+Proof.
+  reflexivity.
+Qed.
+
 Lemma rev_acc_and_rest_list_connection': forall (Shape : Type) (Pos : Shape -> Type) (A : Type)
   (xs : List Shape Pos A) (facc : Free Shape Pos (List Shape Pos A)),  
   rev (pure xs) facc = append (reverse (pure xs)) facc.
@@ -24,11 +35,9 @@ Proof.
   induction xs as [ | x fxs' ] using List_Ind; intros.
   - reflexivity.
   - induction fxs' as [ xs' | sh pos ] using Free_Ind.
-    + simplify2 H as IHxs'. simpl. simpl in IHxs'. rewrite IHxs'. rewrite IHxs'. 
-      assert (H : rev_0 Shape Pos xs' (Cons Shape Pos x (Nil Shape Pos)) = 
-           append (rev_0 Shape Pos xs' (Nil Shape Pos)) (Cons Shape Pos x (Nil Shape Pos))).
-      {rewrite IHxs'. reflexivity. }
-      rewrite H. rewrite append_nil. rewrite <- append_assoc. reflexivity.
+    + simplify2 H as IHxs'. simpl. simpl in IHxs'. rewrite IHxs'. 
+      rewrite IHxs' with (facc := Cons x Nil).
+      rewrite <- append_assoc. reflexivity.
     + simpl. f_equal. extensionality x0. simplify2 H0 as H0'. apply H0'.
 Qed.
 
@@ -51,10 +60,8 @@ Proof.
   - reflexivity.
   - induction fxs' as [ xs' | sh pos ] using Free_Ind.
     + simplify H as IHxs'. simpl reverseNaive. simpl reverse.
-      assert  (H : rev_0 Shape Pos xs' (Cons Shape Pos x (Nil Shape Pos)) = 
-                   rev (pure xs') (Cons Shape Pos x (Nil Shape Pos))).
-      {reflexivity. }
-      rewrite H. rewrite rev_acc_and_rest_list_connection. rewrite IHxs'. reflexivity.
+      rewrite rev_0_rev.
+      rewrite rev_acc_and_rest_list_connection. rewrite IHxs'. reflexivity.
     + simpl. f_equal. extensionality x0. simplify2 H0 as H0'. apply H0'.
 Qed.
 
@@ -68,14 +75,72 @@ Proof.
   - simpl. f_equal. extensionality x. apply H.
 Qed.
 
-Theorem rev_inv_rev: quickCheck (@prop_rev_is_rev_inv Identity.Shape Identity.Pos).
+End reverseIsReverseNaive.
+
+Section reverse_is_involution.
+
+(*in appendProofs kopieren*)
+  Lemma rewrite_Cons:
+  forall (Shape : Type) (Pos : Shape -> Type) (A : Type)
+  (fx : Free Shape Pos A) (fxs : Free Shape Pos (List Shape Pos A)),
+    pure (cons fx fxs) = append (Cons fx Nil) fxs.
+  Proof.
+  reflexivity.
+  Qed.  
+
+Lemma reverseNaive_0_reverseNaive: forall (Shape : Type) (Pos : Shape -> Type) (A : Type)
+  (xs : List Shape Pos A),
+  reverseNaive_0 xs = reverseNaive (pure xs).
 Proof.
-  simpl.
-  intros A totalList.
-  induction totalList as [ xs | [] ] using Free_Ind.
-  - induction xs as [ | x [xs' | []]] using List_Ind.
+  reflexivity.
+Qed.
+
+Lemma reverseNaive_append : forall (A : Type)
+  (fxs fys : Free Identity.Shape Identity.Pos (List Identity.Shape Identity.Pos A)),
+      reverseNaive (append fxs fys) = append (reverseNaive fys) (reverseNaive fxs).
+Proof.
+intros A fxs.
+destruct fxs as [ xs | [] _ ].
+- induction xs as [| fx fxs' IHfxs'] using List_Ind; intros.
+  + rewrite append_nil. simpl. reflexivity.
+  + destruct fxs' as [ xs' | [] pf].
+    * simplify2 IHfxs' as IHxs'. simpl reverseNaive at 3. rewrite reverseNaive_0_reverseNaive.
+      rewrite append_assoc.
+       rewrite <- IHxs'. reflexivity.
+Qed.
+
+Theorem reverseNaive_is_involution: forall (A : Type)
+ (fxs : Free Identity.Shape Identity.Pos (List Identity.Shape Identity.Pos A)),
+  reverseNaive (reverseNaive fxs) = fxs.
+Proof.
+  intros A fxs.
+  destruct fxs as [ xs | [] _ ].
+  - induction xs as [ | fx fxs' IHfxs' ] using List_Ind.
     + reflexivity.
-    + simplify H as H'. simpl.
-Admitted.
+    + destruct fxs' as [ xs' | [] pf].
+      * simplify2 IHfxs' as IHxs'. simpl. rewrite reverseNaive_append.
+        simpl in IHxs'. rewrite IHxs'. reflexivity.
+Qed.
+
+Theorem reverse_is_involution: quickCheck (@prop_rev_is_rev_inv Identity.Shape Identity.Pos).
+Proof.
+  simpl.
+  intros A fxs.
+  do 2 rewrite reverse_is_reverseNaive. 
+  apply reverseNaive_is_involution.
+Qed.
+
+End reverse_is_involution.
+
+Section minus_is_plus_inverse.
+
+Theorem minus_is_plus_inv: quickCheck (@prop_minus_is_plus_inv Identity.Shape Identity.Pos).
+Proof.
+  simpl.
+  intros fx fy.
+  destruct fx as [ x | [] _ ].
+  induction x as [ _ | 
+
+
+End minus_is_plus_inverse.
 
-Section reverseIsReverseNaive.
\ No newline at end of file

From fc37d4baf7d316b6b996ef76ea8ac9766196fb68 Mon Sep 17 00:00:00 2001
From: Johanna <jo-hanna_menzel@live.de>
Date: Mon, 29 Jun 2020 12:20:58 +0200
Subject: [PATCH 08/16] Add property that minus is the inverse of plus for
 peano numbers

---
 example/CaseStudyMorallyCorrect/FastAndLooseReasoning.hs | 3 +++
 .../CaseStudyMorallyCorrect/Output/FastLooseBasic.json   | 9 +++++++++
 example/CaseStudyMorallyCorrect/Output/FastLooseBasic.v  | 5 +++++
 3 files changed, 17 insertions(+)

diff --git a/example/CaseStudyMorallyCorrect/FastAndLooseReasoning.hs b/example/CaseStudyMorallyCorrect/FastAndLooseReasoning.hs
index 1d059448..79cb4f85 100644
--- a/example/CaseStudyMorallyCorrect/FastAndLooseReasoning.hs
+++ b/example/CaseStudyMorallyCorrect/FastAndLooseReasoning.hs
@@ -47,3 +47,6 @@ prop_reverse_is_reverseNaive xs = reverse xs === reverseNaive xs
 
 prop_rev_is_rev_inv :: [a] -> Property
 prop_rev_is_rev_inv xs = reverse (reverse xs) === xs
+
+prop_minus_is_plus_inv :: Peano -> Peano -> Property
+prop_minus_is_plus_inv x y = minus (plus y x) y === x
diff --git a/example/CaseStudyMorallyCorrect/Output/FastLooseBasic.json b/example/CaseStudyMorallyCorrect/Output/FastLooseBasic.json
index f269c4c4..009ed53e 100644
--- a/example/CaseStudyMorallyCorrect/Output/FastLooseBasic.json
+++ b/example/CaseStudyMorallyCorrect/Output/FastLooseBasic.json
@@ -12,6 +12,7 @@
         "FastLooseBasic.minus",
         "FastLooseBasic.plus",
         "FastLooseBasic.pred",
+        "FastLooseBasic.prop_minus_is_plus_inv",
         "FastLooseBasic.prop_rev_is_rev_inv",
         "FastLooseBasic.prop_reverse_is_reverseNaive",
         "FastLooseBasic.rev",
@@ -203,6 +204,14 @@
             "partial": false,
             "haskell-name": "FastLooseBasic.pred"
         },
+        {
+            "arity": 2,
+            "haskell-type": "FastLooseBasic.Peano -> FastLooseBasic.Peano -> Test.QuickCheck.Property",
+            "coq-name": "prop_minus_is_plus_inv",
+            "needs-free-args": true,
+            "partial": false,
+            "haskell-name": "FastLooseBasic.prop_minus_is_plus_inv"
+        },
         {
             "arity": 1,
             "haskell-type": "Prelude.([]) a -> Test.QuickCheck.Property",
diff --git a/example/CaseStudyMorallyCorrect/Output/FastLooseBasic.v b/example/CaseStudyMorallyCorrect/Output/FastLooseBasic.v
index a2c2b43b..3fe28e8e 100644
--- a/example/CaseStudyMorallyCorrect/Output/FastLooseBasic.v
+++ b/example/CaseStudyMorallyCorrect/Output/FastLooseBasic.v
@@ -137,6 +137,11 @@ Definition plus (Shape : Type) (Pos : Shape -> Type) (x_0
   @foldPeano Shape Pos (Peano Shape Pos) (pure (fun x_2 => S Shape Pos x_2)) x_0
                                          x_1.
 
+Definition prop_minus_is_plus_inv (Shape : Type) (Pos : Shape -> Type) (x
+    : Free Shape Pos (Peano Shape Pos)) (y : Free Shape Pos (Peano Shape Pos))
+   : Free Shape Pos (Property Shape Pos) :=
+  @eqProp Shape Pos (Peano Shape Pos) (minus Shape Pos (plus Shape Pos y x) y) x.
+
 Definition comp (Shape : Type) (Pos : Shape -> Type) {b c a : Type} (g
     : Free Shape Pos (Free Shape Pos b -> Free Shape Pos c)) (f
     : Free Shape Pos (Free Shape Pos a -> Free Shape Pos b)) (a0

From 37bdf1e70cea82667ab1f5da762208636439d26c Mon Sep 17 00:00:00 2001
From: Johanna <jo-hanna_menzel@live.de>
Date: Tue, 30 Jun 2020 13:16:18 +0200
Subject: [PATCH 09/16] Prove that minus is pulus inverse

---
 .../CaseStudyMorallyCorrect/Output/PeanoInd.v | 92 +++++++++++++++++++
 .../CaseStudyMorallyCorrect/Output/Proofs.v   | 75 ++++++++++++++-
 2 files changed, 164 insertions(+), 3 deletions(-)
 create mode 100644 example/CaseStudyMorallyCorrect/Output/PeanoInd.v

diff --git a/example/CaseStudyMorallyCorrect/Output/PeanoInd.v b/example/CaseStudyMorallyCorrect/Output/PeanoInd.v
new file mode 100644
index 00000000..725ea498
--- /dev/null
+++ b/example/CaseStudyMorallyCorrect/Output/PeanoInd.v
@@ -0,0 +1,92 @@
+From Base Require Import Free.
+From Generated Require Import FastLooseBasic.
+
+Require Import Coq.Program.Equality.
+
+Arguments zero  {Shape} {Pos}.
+Arguments s {Shape} {Pos} _.
+
+(* Induction principle for peanos *)
+
+Section PeanoInd.
+
+  Variable Shape : Type.
+  Variable Pos : Shape -> Type.
+
+  Variable P : Peano Shape Pos -> Prop.
+
+  Hypothesis zeroP : P zero.
+
+  Hypothesis sP : forall (fx : Free Shape Pos (Peano Shape Pos)),
+      ForFree Shape Pos (Peano Shape Pos) P fx -> P (s fx).
+
+  Fixpoint Peano_Ind (p : Peano Shape Pos) : P p.
+  Proof.
+    destruct p.
+    - apply zeroP.
+    - apply sP.
+      apply (ForFree_forall Shape Pos). intros x HIn.
+      induction f using Free_Ind.
+      + inversion HIn; subst. apply Peano_Ind.
+      + dependent destruction HIn; subst. destruct H0 as [ p ].
+        apply H with (p := p). apply H0.
+  Defined.
+
+End PeanoInd.
+
+(* Induction principle for peanos inside the Free monad. *)
+
+Section FreePeanoRect.
+
+  Variable Shape : Type.
+  Variable Pos : Shape -> Type.
+  Variable PF : Free Shape Pos (Peano Shape Pos) -> Type.
+  Variable P : Peano Shape Pos -> Type.
+
+  Hypothesis ZeroFP : P zero.
+  Hypothesis SFP : forall fx, PF fx -> P (s fx).
+  Hypothesis PurePeanoF : forall xs, P xs -> PF (pure xs).
+  Hypothesis ImpureP :
+    forall (s : Shape)
+           (pf : Pos s -> Free Shape Pos (Peano Shape Pos)),
+    (forall p, PF (pf p)) -> PF (impure s pf).
+
+  Fixpoint Peano_Rect (x: Peano Shape Pos) : P x :=
+    let fix aux (fx: Free Shape Pos (Peano Shape Pos)) : PF fx :=
+        match fx with
+        | pure x => PurePeanoF x (Peano_Rect x)
+        | impure sh pf => ImpureP sh pf (fun p => aux (pf p))
+        end
+    in match x with
+       | zero => ZeroFP
+       | s fx => SFP fx (aux fx)
+       end.
+
+  Fixpoint FreePeano_rect (fx: Free Shape Pos (Peano Shape Pos)) : PF fx :=
+    match fx with
+    | pure x => PurePeanoF x (Peano_Rect x)
+    | impure sh pf => ImpureP sh pf (fun p => FreePeano_rect (pf p))
+    end.
+
+End FreePeanoRect.
+
+Section FreePeanoInd.
+
+  Variable Shape : Type.
+  Variable Pos : Shape -> Type.
+  Variable PF : Free Shape Pos (Peano Shape Pos) -> Type.
+  Variable P : Peano Shape Pos -> Type.
+
+  Hypothesis ZeroFP : P zero.
+  Hypothesis SFP : forall fx, PF fx -> P (s fx).
+  Hypothesis PurePeanoF : forall xs, P xs -> PF (pure xs).
+  Hypothesis ImpureP :
+    forall (s : Shape)
+           (pf : Pos s -> Free Shape Pos (Peano Shape Pos)),
+    (forall p, PF (pf p)) -> PF (impure s pf).
+
+
+  Definition FreePeano_ind (fx: Free Shape Pos (Peano Shape Pos)) : PF fx :=
+    FreePeano_rect Shape Pos PF P ZeroFP SFP PurePeanoF ImpureP fx.
+
+End FreePeanoInd.
diff --git a/example/CaseStudyMorallyCorrect/Output/Proofs.v b/example/CaseStudyMorallyCorrect/Output/Proofs.v
index 4986b763..3e3c764c 100644
--- a/example/CaseStudyMorallyCorrect/Output/Proofs.v
+++ b/example/CaseStudyMorallyCorrect/Output/Proofs.v
@@ -5,6 +5,7 @@ From Base Require Import Prelude.List.
 From Generated Require Import FastLooseBasic.
 From Generated Require Import AppendProofs.
 From Generated Require Import Simplify.
+From Generated Require Import PeanoInd.
 Require Import Coq.Logic.FunctionalExtensionality.
 
 Set Implicit Arguments.
@@ -17,6 +18,9 @@ Arguments reverseNaive_0 {_} {_} {_} _ .
 Arguments append {_} {_} {_} _ _.
 Arguments Nil {_} {_} {_}.
 Arguments Cons {_} {_} {_} _ _.
+Arguments plus {_} {_} _ _.
+Arguments minus {_} {_} _ _.
+Arguments pred {_} {_} _.
 
 Section reverseIsReverseNaive.
 
@@ -134,13 +138,78 @@ End reverse_is_involution.
 
 Section minus_is_plus_inverse.
 
-Theorem minus_is_plus_inv: quickCheck (@prop_minus_is_plus_inv Identity.Shape Identity.Pos).
+Lemma plus_zero': forall (Shape : Type) (Pos : Shape -> Type)
+  (x : Peano Shape Pos),
+  plus (pure zero) (pure x) = (pure x).
+Proof.
+  intros Shape Pos x.
+  induction x as [ | fx' ] using Peano_Ind.
+  - reflexivity.
+  - induction fx' as [ x' | sh pf ] using Free_Ind.
+    + simplify2 H as H'. simpl plus. simpl in H'. rewrite H'.
+      reflexivity.
+    + simpl. unfold S. do 3 apply f_equal. extensionality x. simplify2 H as IH.
+      apply IH.
+Qed.
+
+Lemma plus_zero: forall (Shape : Type) (Pos : Shape -> Type)
+  (fx : Free Shape Pos (Peano Shape Pos)),
+  plus (pure zero) fx = fx.
+Proof.
+  intros Shape Pos fx.
+  induction fx as [ x | pf sh ] using Free_Ind.
+  - apply plus_zero'.
+  - simpl. f_equal. extensionality x. apply H.
+Qed.
+
+Lemma plus_s : forall (fx fy : Free Identity.Shape Identity.Pos (Peano Identity.Shape Identity.Pos)),
+  plus (pure (s fy)) fx = pure (s (plus fy fx)).
 Proof.
-  simpl.
   intros fx fy.
   destruct fx as [ x | [] _ ].
-  induction x as [ _ | 
+  induction x as [ | fx' IHfx' ] using Peano_Ind.
+  - reflexivity.
+  - destruct fx' as [ x' | [] _ ].
+    + simplify2 IHfx' as IH. simpl. simpl in IH.
+      rewrite IH. reflexivity.
+Qed.
 
+Lemma minus_pred : forall (Shape : Type) (Pos : Shape -> Type)
+  (fy fx: Free Shape Pos (Peano Shape Pos)) ,
+  minus fx (pure (s fy)) = minus (pred fx) fy.
+Proof.
+  intros Shape Pos fy fx.
+  induction fy as [ y | sh pos ] using Free_Ind.
+  - induction y as [ | fy' IHfy'] using Peano_Ind. 
+    + reflexivity.
+    + induction fy' as [ y' | sh pos ] using Free_Ind.
+      * simplify2 IHfy' as IH. simpl. simpl in IH. rewrite IH. reflexivity.
+      * simpl. f_equal. extensionality x. simplify2 H as IH. apply IH.
+  - simpl. f_equal. extensionality x. apply H.
+Qed.
+
+Lemma pred_succ: forall (Shape : Type) (Pos : Shape -> Type)
+  (fx: Free Shape Pos (Peano Shape Pos)),
+   pred (pure (s fx)) = fx.
+Proof.
+  intros Shape Pos fx.
+  destruct fx as [ x | sh pf ].
+  - destruct x as [ | fx' ].
+    + reflexivity.
+    + destruct fx' as [ x' | sh pf ]; reflexivity.
+  - reflexivity.
+Qed.
+
+Theorem minus_is_plus_inv: quickCheck (@prop_minus_is_plus_inv Identity.Shape Identity.Pos).
+Proof.
+  simpl.
+  intros fx fy.
+  destruct fy as [ y | [] _ ].
+  induction y as [ | fy' IHfy' ] using Peano_Ind. 
+  - simpl.  apply plus_zero.
+  - destruct fy' as [ y' | [] _ ].
+    + simplify2 IHfy' as IH. rewrite plus_s. rewrite minus_pred. rewrite pred_succ. apply IH.
+Qed.
 
 End minus_is_plus_inverse.
 

From 31c49194ded86cafdd4aaa357e80cbf4ab13c3f9 Mon Sep 17 00:00:00 2001
From: Johanna <jo-hanna_menzel@live.de>
Date: Thu, 2 Jul 2020 09:39:02 +0200
Subject: [PATCH 10/16] Complete helping lemmas about append

---
 .../Output/AppendProofs.v                     | 32 +++++++++++++++----
 1 file changed, 26 insertions(+), 6 deletions(-)

diff --git a/example/CaseStudyMorallyCorrect/Output/AppendProofs.v b/example/CaseStudyMorallyCorrect/Output/AppendProofs.v
index ad7b7d3e..2fdf1219 100644
--- a/example/CaseStudyMorallyCorrect/Output/AppendProofs.v
+++ b/example/CaseStudyMorallyCorrect/Output/AppendProofs.v
@@ -1,23 +1,34 @@
 From Base Require Import Free.
 From Base Require Import Prelude.List.
+From Generated Require Import Simplify.
 From Generated Require Import FastLooseBasic.
 Require Import Coq.Logic.FunctionalExtensionality.
 
 Set Implicit Arguments.
 
 Arguments append {_} {_} {_} _ _.
+Arguments Nil {_} {_} {_}.
+Arguments Cons {_} {_} {_} _ _.
+
+Lemma rewrite_Cons: forall (Shape : Type) (Pos : Shape -> Type) (A : Type)
+  (fx : Free Shape Pos A) (fxs : Free Shape Pos (List Shape Pos A)),
+  Cons fx fxs = append (Cons fx Nil) fxs.
+Proof.
+  reflexivity.
+Qed. 
 
 Lemma append_assoc' : forall (Shape : Type) (Pos : Shape -> Type) (A : Type)
   (xs : List Shape Pos A) (fys fzs : Free Shape Pos (List Shape Pos A)),
   append (pure xs) (append fys fzs) = append (append (pure xs) fys) fzs.
 Proof.
   intros.
-  induction xs as [| fx fxs IH] using List_Ind.
+  induction xs as [ | fx fxs IHimp ] using List_Ind.
   - reflexivity.
-  - induction fxs as [xs | s pf IHpf] using Free_Ind.
+  - induction fxs as [ xs | s pf IHpf ] using Free_Ind.
     + simpl. f_equal. simplify H as IH'. simpl in IH'. apply IH'.
-    + simpl. do 2 apply f_equal. extensionality x.
-Admitted. 
+    + simpl. do 2 apply f_equal. extensionality x. simplify2 IHimp as IH. 
+      apply IH.
+Qed.
 
 Lemma append_assoc : forall (Shape : Type) (Pos : Shape -> Type) (A : Type)
   (fxs fys fzs : Free Shape Pos (List Shape Pos A)),
@@ -32,9 +43,18 @@ Qed.
 
 Lemma append_nil : forall (Shape : Type) (Pos : Shape -> Type) (A : Type)
   (fxs : Free Shape Pos (List Shape Pos A)),
-  append fxs (Nil Shape Pos) = fxs.
+  append fxs Nil = fxs.
 Proof.
-Admitted.
+  intros Shape Pos A fxs.
+  induction fxs as [ xs | s pf IHpf ] using Free_Ind.
+  + induction xs as [ | fx fxs' IHfxs' ] using List_Ind.
+    - reflexivity.
+    - induction fxs' as [ xs' | s pf IHpf ] using Free_Ind.
+      * simplify IHfxs' as IH. simpl append. simpl in IH. rewrite IH. reflexivity.
+      * simpl. unfold Cons. do 3 apply f_equal. extensionality x. simplify2 IHfxs' as IH. 
+        apply IH.
+  + simpl. f_equal. extensionality x. apply IHpf.
+Qed.
 
 
 

From 3d969bf1d8c25a2a4eee216dfe03ba2d28ebf48f Mon Sep 17 00:00:00 2001
From: Johanna <jo-hanna_menzel@live.de>
Date: Thu, 2 Jul 2020 09:44:46 +0200
Subject: [PATCH 11/16] Use comp in property and draft property for main
 theorem

---
 .../FastAndLooseReasoning.hs                  |  15 +-
 .../Output/FastLooseBasic.json                |  24 +-
 .../Output/FastLooseBasic.v                   | 229 +++++++++++++-----
 3 files changed, 197 insertions(+), 71 deletions(-)

diff --git a/example/CaseStudyMorallyCorrect/FastAndLooseReasoning.hs b/example/CaseStudyMorallyCorrect/FastAndLooseReasoning.hs
index 79cb4f85..ed1d57d9 100644
--- a/example/CaseStudyMorallyCorrect/FastAndLooseReasoning.hs
+++ b/example/CaseStudyMorallyCorrect/FastAndLooseReasoning.hs
@@ -48,5 +48,16 @@ prop_reverse_is_reverseNaive xs = reverse xs === reverseNaive xs
 prop_rev_is_rev_inv :: [a] -> Property
 prop_rev_is_rev_inv xs = reverse (reverse xs) === xs
 
-prop_minus_is_plus_inv :: Peano -> Peano -> Property
-prop_minus_is_plus_inv x y = minus (plus y x) y === x
+prop_minus_plus_inv :: Peano -> Peano -> Property
+prop_minus_plus_inv x y = (comp (\x -> minus x y) (\x -> plus y x)) x === x
+
+prop_map_id :: [a] -> Property
+prop_map_id xs = map id xs === xs
+
+-- prop_morally_correct :: Peano -> [Peano] -> Property
+-- porp_morally_correct y xs =
+--   (comp (comp reverse (map (\x -> minus x y)))
+--         (comp (map (\x -> plus y x)) reverse)
+--     )
+--       xs
+--     === id xs
diff --git a/example/CaseStudyMorallyCorrect/Output/FastLooseBasic.json b/example/CaseStudyMorallyCorrect/Output/FastLooseBasic.json
index 009ed53e..34393eff 100644
--- a/example/CaseStudyMorallyCorrect/Output/FastLooseBasic.json
+++ b/example/CaseStudyMorallyCorrect/Output/FastLooseBasic.json
@@ -11,8 +11,10 @@
         "FastLooseBasic.map",
         "FastLooseBasic.minus",
         "FastLooseBasic.plus",
+        "FastLooseBasic.porp_morally_correct",
         "FastLooseBasic.pred",
-        "FastLooseBasic.prop_minus_is_plus_inv",
+        "FastLooseBasic.prop_map_id",
+        "FastLooseBasic.prop_minus_plus_inv",
         "FastLooseBasic.prop_rev_is_rev_inv",
         "FastLooseBasic.prop_reverse_is_reverseNaive",
         "FastLooseBasic.rev",
@@ -196,6 +198,14 @@
             "partial": false,
             "haskell-name": "FastLooseBasic.plus"
         },
+        {
+            "arity": 2,
+            "haskell-type": "FastLooseBasic.Peano -> Prelude.([]) FastLooseBasic.Peano -> Test.QuickCheck.Property",
+            "coq-name": "porp_morally_correct",
+            "needs-free-args": true,
+            "partial": false,
+            "haskell-name": "FastLooseBasic.porp_morally_correct"
+        },
         {
             "arity": 1,
             "haskell-type": "FastLooseBasic.Peano -> FastLooseBasic.Peano",
@@ -204,13 +214,21 @@
             "partial": false,
             "haskell-name": "FastLooseBasic.pred"
         },
+        {
+            "arity": 1,
+            "haskell-type": "Prelude.([]) a -> Test.QuickCheck.Property",
+            "coq-name": "prop_map_id",
+            "needs-free-args": true,
+            "partial": false,
+            "haskell-name": "FastLooseBasic.prop_map_id"
+        },
         {
             "arity": 2,
             "haskell-type": "FastLooseBasic.Peano -> FastLooseBasic.Peano -> Test.QuickCheck.Property",
-            "coq-name": "prop_minus_is_plus_inv",
+            "coq-name": "prop_minus_plus_inv",
             "needs-free-args": true,
             "partial": false,
-            "haskell-name": "FastLooseBasic.prop_minus_is_plus_inv"
+            "haskell-name": "FastLooseBasic.prop_minus_plus_inv"
         },
         {
             "arity": 1,
diff --git a/example/CaseStudyMorallyCorrect/Output/FastLooseBasic.v b/example/CaseStudyMorallyCorrect/Output/FastLooseBasic.v
index 3fe28e8e..2f93d65d 100644
--- a/example/CaseStudyMorallyCorrect/Output/FastLooseBasic.v
+++ b/example/CaseStudyMorallyCorrect/Output/FastLooseBasic.v
@@ -31,22 +31,22 @@ Definition S (Shape : Type) (Pos : Shape -> Type) (x_0
 
 (* Helper functions for rev *)
 
-Fixpoint rev_0 (Shape : Type) (Pos : Shape -> Type) {t0 : Type} (a11
-                 : List Shape Pos t0) (a12 : Free Shape Pos (List Shape Pos t0)) {struct a11}
+Fixpoint rev_0 (Shape : Type) (Pos : Shape -> Type) {t0 : Type} (a15
+                 : List Shape Pos t0) (a16 : Free Shape Pos (List Shape Pos t0)) {struct a15}
            : Free Shape Pos (List Shape Pos t0)
-           := match a11 with
-              | nil => a12
-              | cons a13 a14 =>
-                  a14 >>=
-                  (fun (a14_0 : List Shape Pos t0) =>
-                     @rev_0 Shape Pos t0 a14_0 (@Cons Shape Pos t0 a13 a12))
+           := match a15 with
+              | nil => a16
+              | cons a17 a18 =>
+                  a18 >>=
+                  (fun (a18_0 : List Shape Pos t0) =>
+                     @rev_0 Shape Pos t0 a18_0 (@Cons Shape Pos t0 a17 a16))
               end.
 
-Definition rev (Shape : Type) (Pos : Shape -> Type) {t0 : Type} (a11
-    : Free Shape Pos (List Shape Pos t0)) (a12
+Definition rev (Shape : Type) (Pos : Shape -> Type) {t0 : Type} (a15
+    : Free Shape Pos (List Shape Pos t0)) (a16
     : Free Shape Pos (List Shape Pos t0))
    : Free Shape Pos (List Shape Pos t0) :=
-  a11 >>= (fun (a11_0 : List Shape Pos t0) => @rev_0 Shape Pos t0 a11_0 a12).
+  a15 >>= (fun (a15_0 : List Shape Pos t0) => @rev_0 Shape Pos t0 a15_0 a16).
 
 Definition reverse (Shape : Type) (Pos : Shape -> Type) {a : Type} (xs
     : Free Shape Pos (List Shape Pos a))
@@ -59,71 +59,77 @@ Definition prop_rev_is_rev_inv (Shape : Type) (Pos : Shape -> Type) {a : Type}
   @eqProp Shape Pos (List Shape Pos a) (@reverse Shape Pos a (@reverse Shape Pos a
                                                               xs)) xs.
 
-Definition pred (Shape : Type) (Pos : Shape -> Type) (a23
+Definition pred (Shape : Type) (Pos : Shape -> Type) (a27
     : Free Shape Pos (Peano Shape Pos))
    : Free Shape Pos (Peano Shape Pos) :=
-  a23 >>=
-  (fun a23_0 => match a23_0 with | zero => Zero Shape Pos | s a24 => a24 end).
+  a27 >>=
+  (fun a27_0 => match a27_0 with | zero => Zero Shape Pos | s a28 => a28 end).
 
 Section section_map_0.
 (* Constant arguments for map *)
 Variable Shape : Type.
 Variable Pos : Shape -> Type.
 Variable a_0 b_0 : Type.
-Variable a17_0 : Free Shape Pos (Free Shape Pos a_0 -> Free Shape Pos b_0).
+Variable a21_0 : Free Shape Pos (Free Shape Pos a_0 -> Free Shape Pos b_0).
 (* Helper functions for map *)
-Fixpoint map_1 (a18 : List Shape Pos a_0) {struct a18} : Free Shape Pos (List
+Fixpoint map_1 (a22 : List Shape Pos a_0) {struct a22} : Free Shape Pos (List
                                                                Shape Pos b_0)
-           := match a18 with
+           := match a22 with
               | nil => @Nil Shape Pos b_0
-              | cons a19 a20 =>
-                  @Cons Shape Pos b_0 (a17_0 >>= (fun a17_1 => a17_1 a19)) (a20 >>=
-                                       (fun (a20_0 : List Shape Pos a_0) => map_1 a20_0))
+              | cons a23 a24 =>
+                  @Cons Shape Pos b_0 (a21_0 >>= (fun a21_1 => a21_1 a23)) (a24 >>=
+                                       (fun (a24_0 : List Shape Pos a_0) => map_1 a24_0))
               end.
 (* Main functions for map *)
-Definition map_0 (a18 : Free Shape Pos (List Shape Pos a_0))
+Definition map_0 (a22 : Free Shape Pos (List Shape Pos a_0))
    : Free Shape Pos (List Shape Pos b_0) :=
-  a18 >>= (fun (a18_0 : List Shape Pos a_0) => map_1 a18_0).
+  a22 >>= (fun (a22_0 : List Shape Pos a_0) => map_1 a22_0).
 End section_map_0.
 
-Definition map (Shape : Type) (Pos : Shape -> Type) {a b : Type} (a17
-    : Free Shape Pos (Free Shape Pos a -> Free Shape Pos b)) (a18
+Definition map (Shape : Type) (Pos : Shape -> Type) {a b : Type} (a21
+    : Free Shape Pos (Free Shape Pos a -> Free Shape Pos b)) (a22
     : Free Shape Pos (List Shape Pos a))
    : Free Shape Pos (List Shape Pos b) :=
-  map_0 Shape Pos a b a17 a18.
+  map_0 Shape Pos a b a21 a22.
 
 Definition id (Shape : Type) (Pos : Shape -> Type) {a : Type} (a0
     : Free Shape Pos a)
    : Free Shape Pos a :=
   a0.
 
+Definition prop_map_id (Shape : Type) (Pos : Shape -> Type) {a : Type} (xs
+    : Free Shape Pos (List Shape Pos a))
+   : Free Shape Pos (Property Shape Pos) :=
+  @eqProp Shape Pos (List Shape Pos a) (@map Shape Pos a a (pure (fun x_0 =>
+                                                                    @id Shape Pos a x_0)) xs) xs.
+
 Section section_foldPeano_0.
 (* Constant arguments for foldPeano *)
 Variable Shape : Type.
 Variable Pos : Shape -> Type.
 Variable a_0 : Type.
-Variable a27_0 : Free Shape Pos a_0.
-Variable a26_0 : Free Shape Pos (Free Shape Pos a_0 -> Free Shape Pos a_0).
+Variable a31_0 : Free Shape Pos a_0.
+Variable a30_0 : Free Shape Pos (Free Shape Pos a_0 -> Free Shape Pos a_0).
 (* Helper functions for foldPeano *)
-Fixpoint foldPeano_1 (a28 : Peano Shape Pos) {struct a28} : Free Shape Pos a_0
-           := match a28 with
-              | zero => a27_0
-              | s a29 =>
-                  a26_0 >>=
-                  (fun a26_1 =>
-                     a26_1 (a29 >>= (fun (a29_0 : Peano Shape Pos) => foldPeano_1 a29_0)))
+Fixpoint foldPeano_1 (a32 : Peano Shape Pos) {struct a32} : Free Shape Pos a_0
+           := match a32 with
+              | zero => a31_0
+              | s a33 =>
+                  a30_0 >>=
+                  (fun a30_1 =>
+                     a30_1 (a33 >>= (fun (a33_0 : Peano Shape Pos) => foldPeano_1 a33_0)))
               end.
 (* Main functions for foldPeano *)
-Definition foldPeano_0 (a28 : Free Shape Pos (Peano Shape Pos))
+Definition foldPeano_0 (a32 : Free Shape Pos (Peano Shape Pos))
    : Free Shape Pos a_0 :=
-  a28 >>= (fun (a28_0 : Peano Shape Pos) => foldPeano_1 a28_0).
+  a32 >>= (fun (a32_0 : Peano Shape Pos) => foldPeano_1 a32_0).
 End section_foldPeano_0.
 
-Definition foldPeano (Shape : Type) (Pos : Shape -> Type) {a : Type} (a26
-    : Free Shape Pos (Free Shape Pos a -> Free Shape Pos a)) (a27
-    : Free Shape Pos a) (a28 : Free Shape Pos (Peano Shape Pos))
+Definition foldPeano (Shape : Type) (Pos : Shape -> Type) {a : Type} (a30
+    : Free Shape Pos (Free Shape Pos a -> Free Shape Pos a)) (a31
+    : Free Shape Pos a) (a32 : Free Shape Pos (Peano Shape Pos))
    : Free Shape Pos a :=
-  foldPeano_0 Shape Pos a a27 a26 a28.
+  foldPeano_0 Shape Pos a a31 a30 a32.
 
 Definition minus (Shape : Type) (Pos : Shape -> Type) (x_0
     : Free Shape Pos (Peano Shape Pos)) (x_1 : Free Shape Pos (Peano Shape Pos))
@@ -137,11 +143,6 @@ Definition plus (Shape : Type) (Pos : Shape -> Type) (x_0
   @foldPeano Shape Pos (Peano Shape Pos) (pure (fun x_2 => S Shape Pos x_2)) x_0
                                          x_1.
 
-Definition prop_minus_is_plus_inv (Shape : Type) (Pos : Shape -> Type) (x
-    : Free Shape Pos (Peano Shape Pos)) (y : Free Shape Pos (Peano Shape Pos))
-   : Free Shape Pos (Property Shape Pos) :=
-  @eqProp Shape Pos (Peano Shape Pos) (minus Shape Pos (plus Shape Pos y x) y) x.
-
 Definition comp (Shape : Type) (Pos : Shape -> Type) {b c a : Type} (g
     : Free Shape Pos (Free Shape Pos b -> Free Shape Pos c)) (f
     : Free Shape Pos (Free Shape Pos a -> Free Shape Pos b)) (a0
@@ -149,48 +150,144 @@ Definition comp (Shape : Type) (Pos : Shape -> Type) {b c a : Type} (g
    : Free Shape Pos c :=
   g >>= (fun g_0 => g_0 (f >>= (fun f_0 => f_0 a0))).
 
+Definition porp_morally_correct (Shape : Type) (Pos : Shape -> Type) (y
+    : Free Shape Pos (Peano Shape Pos)) (xs
+    : Free Shape Pos (List Shape Pos (Peano Shape Pos)))
+   : Free Shape Pos (Property Shape Pos) :=
+  @eqProp Shape Pos (List Shape Pos (Peano Shape Pos)) (@comp Shape Pos (List
+                                                         Shape Pos (Peano Shape Pos)) (List Shape Pos (Peano Shape Pos))
+                                                        (List Shape Pos (Peano Shape Pos)) (pure (fun x_0 =>
+                                                                                                    @comp Shape Pos
+                                                                                                    (List Shape Pos
+                                                                                                          (Peano Shape
+                                                                                                                 Pos))
+                                                                                                    (List Shape Pos
+                                                                                                          (Peano Shape
+                                                                                                                 Pos))
+                                                                                                    (List Shape Pos
+                                                                                                          (Peano Shape
+                                                                                                                 Pos))
+                                                                                                    (pure (fun x_1 =>
+                                                                                                             @reverse
+                                                                                                             Shape Pos
+                                                                                                             (Peano
+                                                                                                              Shape Pos)
+                                                                                                             x_1)) (pure
+                                                                                                     (fun x_1 =>
+                                                                                                        @map Shape Pos
+                                                                                                        (Peano Shape
+                                                                                                               Pos)
+                                                                                                        (Peano Shape
+                                                                                                               Pos)
+                                                                                                        (pure (fun (a2
+                                                                                                                 : Free
+                                                                                                                   Shape
+                                                                                                                   Pos
+                                                                                                                   (Peano
+                                                                                                                    Shape
+                                                                                                                    Pos)) =>
+                                                                                                                 minus
+                                                                                                                 Shape
+                                                                                                                 Pos a2
+                                                                                                                 y))
+                                                                                                        x_1)) x_0))
+                                                                                           (pure (fun x_0 =>
+                                                                                                    @comp Shape Pos
+                                                                                                    (List Shape Pos
+                                                                                                          (Peano Shape
+                                                                                                                 Pos))
+                                                                                                    (List Shape Pos
+                                                                                                          (Peano Shape
+                                                                                                                 Pos))
+                                                                                                    (List Shape Pos
+                                                                                                          (Peano Shape
+                                                                                                                 Pos))
+                                                                                                    (pure (fun x_1 =>
+                                                                                                             @map Shape
+                                                                                                             Pos (Peano
+                                                                                                              Shape Pos)
+                                                                                                             (Peano
+                                                                                                              Shape Pos)
+                                                                                                             (pure
+                                                                                                              (fun (a3
+                                                                                                                 : Free
+                                                                                                                   Shape
+                                                                                                                   Pos
+                                                                                                                   (Peano
+                                                                                                                    Shape
+                                                                                                                    Pos)) =>
+                                                                                                                 plus
+                                                                                                                 Shape
+                                                                                                                 Pos y
+                                                                                                                 a3))
+                                                                                                             x_1)) (pure
+                                                                                                     (fun x_1 =>
+                                                                                                        @reverse Shape
+                                                                                                        Pos (Peano Shape
+                                                                                                                   Pos)
+                                                                                                        x_1)) x_0)) xs)
+                                                       (@id Shape Pos (List Shape Pos (Peano Shape Pos)) xs).
+
+Definition prop_minus_plus_inv (Shape : Type) (Pos : Shape -> Type) (x
+    : Free Shape Pos (Peano Shape Pos)) (y : Free Shape Pos (Peano Shape Pos))
+   : Free Shape Pos (Property Shape Pos) :=
+  @eqProp Shape Pos (Peano Shape Pos) (@comp Shape Pos (Peano Shape Pos) (Peano
+                                        Shape Pos) (Peano Shape Pos) (pure (fun (a0
+                                                                              : Free Shape Pos (Peano Shape Pos)) =>
+                                                                              minus Shape Pos a0 y)) (pure (fun (a1
+                                                                                                              : Free
+                                                                                                                Shape
+                                                                                                                Pos
+                                                                                                                (Peano
+                                                                                                                 Shape
+                                                                                                                 Pos)) =>
+                                                                                                              plus Shape
+                                                                                                                   Pos y
+                                                                                                                   a1))
+                                                                     x) x.
+
 Section section_append_0.
 (* Constant arguments for append *)
 Variable Shape : Type.
 Variable Pos : Shape -> Type.
 Variable a_0 : Type.
-Variable a1_0 : Free Shape Pos (List Shape Pos a_0).
+Variable a5_0 : Free Shape Pos (List Shape Pos a_0).
 (* Helper functions for append *)
-Fixpoint append_1 (a0 : List Shape Pos a_0) {struct a0} : Free Shape Pos (List
+Fixpoint append_1 (a4 : List Shape Pos a_0) {struct a4} : Free Shape Pos (List
                                                                 Shape Pos a_0)
-           := match a0 with
-              | nil => a1_0
-              | cons a2 a3 =>
-                  @Cons Shape Pos a_0 a2 (a3 >>=
-                                       (fun (a3_0 : List Shape Pos a_0) => append_1 a3_0))
+           := match a4 with
+              | nil => a5_0
+              | cons a6 a7 =>
+                  @Cons Shape Pos a_0 a6 (a7 >>=
+                                       (fun (a7_0 : List Shape Pos a_0) => append_1 a7_0))
               end.
 (* Main functions for append *)
-Definition append_0 (a0 : Free Shape Pos (List Shape Pos a_0))
+Definition append_0 (a4 : Free Shape Pos (List Shape Pos a_0))
    : Free Shape Pos (List Shape Pos a_0) :=
-  a0 >>= (fun (a0_0 : List Shape Pos a_0) => append_1 a0_0).
+  a4 >>= (fun (a4_0 : List Shape Pos a_0) => append_1 a4_0).
 End section_append_0.
 
-Definition append (Shape : Type) (Pos : Shape -> Type) {a : Type} (a0
-    : Free Shape Pos (List Shape Pos a)) (a1 : Free Shape Pos (List Shape Pos a))
+Definition append (Shape : Type) (Pos : Shape -> Type) {a : Type} (a4
+    : Free Shape Pos (List Shape Pos a)) (a5 : Free Shape Pos (List Shape Pos a))
    : Free Shape Pos (List Shape Pos a) :=
-  append_0 Shape Pos a a1 a0.
+  append_0 Shape Pos a a5 a4.
 
 (* Helper functions for reverseNaive *)
 
-Fixpoint reverseNaive_0 (Shape : Type) (Pos : Shape -> Type) {a : Type} (a6
-                          : List Shape Pos a) {struct a6} : Free Shape Pos (List Shape Pos a)
-           := match a6 with
+Fixpoint reverseNaive_0 (Shape : Type) (Pos : Shape -> Type) {a : Type} (a10
+                          : List Shape Pos a) {struct a10} : Free Shape Pos (List Shape Pos a)
+           := match a10 with
               | nil => @Nil Shape Pos a
-              | cons a7 a8 =>
-                  @append Shape Pos a (a8 >>=
-                                       (fun (a8_0 : List Shape Pos a) => @reverseNaive_0 Shape Pos a a8_0)) (@Cons
-                                       Shape Pos a a7 (@Nil Shape Pos a))
+              | cons a11 a12 =>
+                  @append Shape Pos a (a12 >>=
+                                       (fun (a12_0 : List Shape Pos a) => @reverseNaive_0 Shape Pos a a12_0)) (@Cons
+                                       Shape Pos a a11 (@Nil Shape Pos a))
               end.
 
-Definition reverseNaive (Shape : Type) (Pos : Shape -> Type) {a : Type} (a6
+Definition reverseNaive (Shape : Type) (Pos : Shape -> Type) {a : Type} (a10
     : Free Shape Pos (List Shape Pos a))
    : Free Shape Pos (List Shape Pos a) :=
-  a6 >>= (fun (a6_0 : List Shape Pos a) => @reverseNaive_0 Shape Pos a a6_0).
+  a10 >>= (fun (a10_0 : List Shape Pos a) => @reverseNaive_0 Shape Pos a a10_0).
 
 Definition prop_reverse_is_reverseNaive (Shape : Type) (Pos : Shape -> Type) {a
    : Type} (xs : Free Shape Pos (List Shape Pos a))

From fd9b7c999d15cda18819de219a3fb8f288e4e29b Mon Sep 17 00:00:00 2001
From: Johanna <jo-hanna_menzel@live.de>
Date: Thu, 2 Jul 2020 09:45:38 +0200
Subject: [PATCH 12/16] Finish proof for self formulated main theorem

---
 .../CaseStudyMorallyCorrect/Output/Proofs.v   | 165 +++++++++++++-----
 1 file changed, 126 insertions(+), 39 deletions(-)

diff --git a/example/CaseStudyMorallyCorrect/Output/Proofs.v b/example/CaseStudyMorallyCorrect/Output/Proofs.v
index 3e3c764c..fb0a1d63 100644
--- a/example/CaseStudyMorallyCorrect/Output/Proofs.v
+++ b/example/CaseStudyMorallyCorrect/Output/Proofs.v
@@ -1,3 +1,4 @@
+
 From Base Require Import Test.QuickCheck.
 From Base Require Import Free.Instance.Identity.
 From Base Require Import Free.
@@ -21,6 +22,11 @@ Arguments Cons {_} {_} {_} _ _.
 Arguments plus {_} {_} _ _.
 Arguments minus {_} {_} _ _.
 Arguments pred {_} {_} _.
+Arguments map {_} {_} {_} {_} _ _.
+Arguments comp {_} {_} {_} {_} {_} _ _.
+Arguments id {_} {_} {_} _.
+Arguments S {_} {_} _.
+Arguments Zero {_} {_}.
 
 Section reverseIsReverseNaive.
 
@@ -36,13 +42,13 @@ Lemma rev_acc_and_rest_list_connection': forall (Shape : Type) (Pos : Shape -> T
   rev (pure xs) facc = append (reverse (pure xs)) facc.
 Proof.
   intros Shape Pos A xs.
-  induction xs as [ | x fxs' ] using List_Ind; intros.
+  induction xs as [ | fx fxs' IHfxs'] using List_Ind; intros facc.
   - reflexivity.
-  - induction fxs' as [ xs' | sh pos ] using Free_Ind.
-    + simplify2 H as IHxs'. simpl. simpl in IHxs'. rewrite IHxs'. 
-      rewrite IHxs' with (facc := Cons x Nil).
+  - induction fxs' as [ xs' | sh pos IHpos] using Free_Ind.
+    + simplify2 IHfxs' as IH. simpl. simpl in IH. rewrite IH. 
+      rewrite IH with (facc := Cons fx Nil).
       rewrite <- append_assoc. reflexivity.
-    + simpl. f_equal. extensionality x0. simplify2 H0 as H0'. apply H0'.
+    + simpl. f_equal. extensionality x. simplify2 IHpos as IH. apply IH.
 Qed.
 
 Lemma rev_acc_and_rest_list_connection: forall (Shape : Type) (Pos : Shape -> Type) (A : Type)
@@ -50,9 +56,9 @@ Lemma rev_acc_and_rest_list_connection: forall (Shape : Type) (Pos : Shape -> Ty
   rev fxs facc = append (reverse fxs) facc.
 Proof.
   intros Shape Pos A fxs facc.
-  induction fxs as [ xs | sh pos ] using Free_Ind.
+  induction fxs as [ xs | sh pos IHpos ] using Free_Ind.
   - apply rev_acc_and_rest_list_connection'.
-  - simpl. f_equal. extensionality x. apply H.
+  - simpl. f_equal. extensionality x. apply IHpos.
 Qed.
 
 Lemma reverse_is_reverseNaive': forall (Shape : Type) (Pos : Shape -> Type) (A : Type)
@@ -60,37 +66,28 @@ Lemma reverse_is_reverseNaive': forall (Shape : Type) (Pos : Shape -> Type) (A :
   reverse (pure xs) = reverseNaive (pure xs).
 Proof.
   intros Shape Pos A xs.
-  induction xs as [ | x fxs' ] using List_Ind.
+  induction xs as [ | fx fxs' IHfxs' ] using List_Ind.
   - reflexivity.
-  - induction fxs' as [ xs' | sh pos ] using Free_Ind.
-    + simplify H as IHxs'. simpl reverseNaive. simpl reverse.
+  - induction fxs' as [ xs' | sh pos IHpos ] using Free_Ind.
+    + simplify IHfxs' as IH. simpl reverseNaive. simpl reverse.
       rewrite rev_0_rev.
-      rewrite rev_acc_and_rest_list_connection. rewrite IHxs'. reflexivity.
-    + simpl. f_equal. extensionality x0. simplify2 H0 as H0'. apply H0'.
+      rewrite rev_acc_and_rest_list_connection. rewrite IH. reflexivity.
+    + simpl. f_equal. extensionality x. simplify2 IHpos as IH. apply IH.
 Qed.
 
-
 Theorem reverse_is_reverseNaive: quickCheck prop_reverse_is_reverseNaive.
 Proof.
   simpl.
   intros Shape Pos A fxs.
-  induction fxs as [ xs | sh pos ] using Free_Ind.
+  induction fxs as [ xs | sh pos IHpos ] using Free_Ind.
   - apply reverse_is_reverseNaive'.
-  - simpl. f_equal. extensionality x. apply H.
+  - simpl. f_equal. extensionality x. apply IHpos.
 Qed.
 
 End reverseIsReverseNaive.
 
-Section reverse_is_involution.
 
-(*in appendProofs kopieren*)
-  Lemma rewrite_Cons:
-  forall (Shape : Type) (Pos : Shape -> Type) (A : Type)
-  (fx : Free Shape Pos A) (fxs : Free Shape Pos (List Shape Pos A)),
-    pure (cons fx fxs) = append (Cons fx Nil) fxs.
-  Proof.
-  reflexivity.
-  Qed.  
+Section reverse_is_involution.
 
 Lemma reverseNaive_0_reverseNaive: forall (Shape : Type) (Pos : Shape -> Type) (A : Type)
   (xs : List Shape Pos A),
@@ -110,7 +107,7 @@ destruct fxs as [ xs | [] _ ].
   + destruct fxs' as [ xs' | [] pf].
     * simplify2 IHfxs' as IHxs'. simpl reverseNaive at 3. rewrite reverseNaive_0_reverseNaive.
       rewrite append_assoc.
-       rewrite <- IHxs'. reflexivity.
+      rewrite <- IHxs'. reflexivity.
 Qed.
 
 Theorem reverseNaive_is_involution: forall (A : Type)
@@ -143,12 +140,12 @@ Lemma plus_zero': forall (Shape : Type) (Pos : Shape -> Type)
   plus (pure zero) (pure x) = (pure x).
 Proof.
   intros Shape Pos x.
-  induction x as [ | fx' ] using Peano_Ind.
+  induction x as [ | fx' IHfx' ] using Peano_Ind.
   - reflexivity.
-  - induction fx' as [ x' | sh pf ] using Free_Ind.
-    + simplify2 H as H'. simpl plus. simpl in H'. rewrite H'.
+  - induction fx' as [ x' | sh pos IHpos ] using Free_Ind.
+    + simplify2 IHfx' as IH. simpl plus. simpl in IH. rewrite IH.
       reflexivity.
-    + simpl. unfold S. do 3 apply f_equal. extensionality x. simplify2 H as IH.
+    + simpl. unfold S. do 3 apply f_equal. extensionality x. simplify2 IHpos as IH.
       apply IH.
 Qed.
 
@@ -157,9 +154,9 @@ Lemma plus_zero: forall (Shape : Type) (Pos : Shape -> Type)
   plus (pure zero) fx = fx.
 Proof.
   intros Shape Pos fx.
-  induction fx as [ x | pf sh ] using Free_Ind.
+  induction fx as [ x | pf sh IHpos ] using Free_Ind.
   - apply plus_zero'.
-  - simpl. f_equal. extensionality x. apply H.
+  - simpl. f_equal. extensionality x. apply IHpos.
 Qed.
 
 Lemma plus_s : forall (fx fy : Free Identity.Shape Identity.Pos (Peano Identity.Shape Identity.Pos)),
@@ -179,13 +176,13 @@ Lemma minus_pred : forall (Shape : Type) (Pos : Shape -> Type)
   minus fx (pure (s fy)) = minus (pred fx) fy.
 Proof.
   intros Shape Pos fy fx.
-  induction fy as [ y | sh pos ] using Free_Ind.
-  - induction y as [ | fy' IHfy'] using Peano_Ind. 
+  induction fy as [ y | sh pos IHpos ] using Free_Ind.
+  - induction y as [ | fy' IHfy' ] using Peano_Ind. 
     + reflexivity.
-    + induction fy' as [ y' | sh pos ] using Free_Ind.
+    + induction fy' as [ y' | sh pos IHpos ] using Free_Ind.
       * simplify2 IHfy' as IH. simpl. simpl in IH. rewrite IH. reflexivity.
-      * simpl. f_equal. extensionality x. simplify2 H as IH. apply IH.
-  - simpl. f_equal. extensionality x. apply H.
+      * simpl. f_equal. extensionality x. simplify2 IHpos as IH. apply IH.
+  - simpl. f_equal. extensionality x. apply IHpos.
 Qed.
 
 Lemma pred_succ: forall (Shape : Type) (Pos : Shape -> Type)
@@ -200,16 +197,106 @@ Proof.
   - reflexivity.
 Qed.
 
-Theorem minus_is_plus_inv: quickCheck (@prop_minus_is_plus_inv Identity.Shape Identity.Pos).
+Theorem minus_is_plus_inv_ext: quickCheck (@prop_minus_plus_inv Identity.Shape Identity.Pos).
 Proof.
-  simpl.
+  simpl quickCheck.
   intros fx fy.
   destruct fy as [ y | [] _ ].
   induction y as [ | fy' IHfy' ] using Peano_Ind. 
-  - simpl.  apply plus_zero.
+  - simpl. apply plus_zero.
   - destruct fy' as [ y' | [] _ ].
     + simplify2 IHfy' as IH. rewrite plus_s. rewrite minus_pred. rewrite pred_succ. apply IH.
 Qed.
 
+Lemma minus_plus_inv: forall (fy : Free Identity.Shape Identity.Pos (Peano Identity.Shape Identity.Pos)),
+  comp (pure (fun fx => minus fx fy)) (pure (fun fx => plus fy fx)) = id.
+Proof.
+  intros fy.
+  extensionality fx.
+  simpl.
+  apply minus_is_plus_inv_ext.
+Qed.
+
+
 End minus_is_plus_inverse.
 
+Section small_helping_lemmas.
+
+Lemma comp_id : forall (Shape : Type) (Pos : Shape -> Type) (A B : Type)
+ (f :(Free Shape Pos A -> Free Shape Pos B)),
+  (pure (comp (pure id) (pure f))) = @pure Shape Pos (Free Shape Pos A -> Free Shape Pos B) f.
+Proof.
+  intros Shape Pos A B ff.
+  f_equal.
+Qed.
+
+Lemma map_fusion : forall (Shape : Type) (Pos : Shape -> Type) (A B C : Type) 
+  (ff : Free Shape Pos (Free Shape Pos B -> Free Shape Pos C))
+  (fg : Free Shape Pos (Free Shape Pos A -> Free Shape Pos B)),
+  comp (pure (map ff)) (pure (map fg)) = map (pure (comp ff fg)).
+Proof.
+  intros Shape Pos A B C ff gg.
+  extensionality fxs.
+  induction fxs as [ xs | sh pos IHpos ] using Free_Ind.
+  - induction xs as [| fx fxs' IHfxs ] using List_Ind.
+    + reflexivity.
+    + induction fxs' as [ xs' | sh pos IHpos ] using Free_Ind.
+      * simplify2 IHfxs as IH. simpl. f_equal. simpl in IH. rewrite <- IH. reflexivity.
+      * simpl. do 2 f_equal. extensionality x. simplify2 IHpos as IH. apply IH.
+  - simpl. f_equal. extensionality x. apply IHpos.
+Qed.
+
+Lemma map_id_ext : quickCheck prop_map_id.
+Proof.
+  simpl.
+  intros Shape Pos A fxs.
+  unfold id.
+  induction fxs as [ xs | sh pos IHpos ] using Free_Ind.
+  - induction xs as [| fx fxs' IHfxs ] using List_Ind.
+    + reflexivity.
+    + induction fxs' as [ xs' | sh pos IHpos ] using Free_Ind.
+      * simplify2 IHfxs as IH. simpl. unfold Cons. do 2 f_equal. simpl in IH. apply IH.
+      * simpl. unfold Cons. do 3 f_equal. extensionality x. simplify2 IHpos as IH. apply IH.
+  - simpl. f_equal. extensionality x. apply IHpos.
+Qed.
+
+Lemma map_id : forall (Shape : Type) (Pos : Shape -> Type) (A : Type),
+  @map Shape Pos A A (pure id) = id.
+Proof.
+  intros Shape Pos A.
+  extensionality fxs.
+  apply map_id_ext.
+Qed.
+
+Lemma compose_assoc : forall (Shape : Type) (Pos : Shape -> Type) (A B C D : Type) 
+  (fcd : Free Shape Pos (Free Shape Pos C -> Free Shape Pos D))
+  (fbc : Free Shape Pos (Free Shape Pos B -> Free Shape Pos C))
+  (fab : Free Shape Pos (Free Shape Pos A -> Free Shape Pos B)),
+  (comp (pure (comp fcd fbc)) fab)  = (comp fcd (pure (comp fbc fab))).
+Proof.
+  intros Shape Pos A B C D fcd fbc fab.
+  destruct fcd as [ cd | sh pos ]; reflexivity.
+Qed.
+
+End small_helping_lemmas.
+
+Section main_proof.
+
+Theorem fancy_id : forall (fy : Free Identity.Shape Identity.Pos (Peano Identity.Shape Identity.Pos))
+  (fxs : Free Identity.Shape Identity.Pos (List Identity.Shape Identity.Pos (Peano Identity.Shape Identity.Pos))),
+  (comp (pure (comp (pure reverse) (pure (map (pure (fun x => minus x fy))))))
+        (pure (comp (pure (map (pure (fun x => plus fy x)))) (pure reverse))))
+   fxs = id fxs.
+Proof.
+  intros fy fxs.
+  rewrite compose_assoc.
+  rewrite <- compose_assoc with (fcd := pure (map (pure (fun x => minus x fy)))).
+  rewrite map_fusion.  
+  rewrite minus_plus_inv.
+  rewrite map_id.
+  rewrite comp_id.
+  simpl. 
+  apply reverse_is_involution.
+Qed.
+
+End main_proof.
\ No newline at end of file

From 818d05b2ae7f5cab9e8d0e0e3fe5044c31fdef5a Mon Sep 17 00:00:00 2001
From: Johanna <jo-hanna_menzel@live.de>
Date: Thu, 2 Jul 2020 09:55:17 +0200
Subject: [PATCH 13/16] Normalize line endings

---
 .../FastAndLooseReasoning.hs                       | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/example/CaseStudyMorallyCorrect/FastAndLooseReasoning.hs b/example/CaseStudyMorallyCorrect/FastAndLooseReasoning.hs
index ed1d57d9..774d35d8 100644
--- a/example/CaseStudyMorallyCorrect/FastAndLooseReasoning.hs
+++ b/example/CaseStudyMorallyCorrect/FastAndLooseReasoning.hs
@@ -54,10 +54,10 @@ prop_minus_plus_inv x y = (comp (\x -> minus x y) (\x -> plus y x)) x === x
 prop_map_id :: [a] -> Property
 prop_map_id xs = map id xs === xs
 
--- prop_morally_correct :: Peano -> [Peano] -> Property
--- porp_morally_correct y xs =
---   (comp (comp reverse (map (\x -> minus x y)))
---         (comp (map (\x -> plus y x)) reverse)
---     )
---       xs
---     === id xs
+-- prop_morally_correct :: Peano -> [Peano] -> Property
+-- porp_morally_correct y xs =
+--   (comp (comp reverse (map (\x -> minus x y)))
+--         (comp (map (\x -> plus y x)) reverse)
+--     )
+--       xs
+--     === id xs

From 1c4681a3702375c35fae9ce4430d8898ea2921cd Mon Sep 17 00:00:00 2001
From: Johanna <jo-hanna_menzel@live.de>
Date: Thu, 2 Jul 2020 10:55:29 +0200
Subject: [PATCH 14/16] Define main theorem as Haskell property

---
 .../FastAndLooseReasoning.hs                  | 14 +++----
 .../Output/FastLooseBasic.json                | 18 ++++-----
 .../Output/FastLooseBasic.v                   | 38 +++++++++----------
 .../CaseStudyMorallyCorrect/Output/Proofs.v   |  7 +++-
 4 files changed, 40 insertions(+), 37 deletions(-)

diff --git a/example/CaseStudyMorallyCorrect/FastAndLooseReasoning.hs b/example/CaseStudyMorallyCorrect/FastAndLooseReasoning.hs
index 774d35d8..3bed1a85 100644
--- a/example/CaseStudyMorallyCorrect/FastAndLooseReasoning.hs
+++ b/example/CaseStudyMorallyCorrect/FastAndLooseReasoning.hs
@@ -54,10 +54,10 @@ prop_minus_plus_inv x y = (comp (\x -> minus x y) (\x -> plus y x)) x === x
 prop_map_id :: [a] -> Property
 prop_map_id xs = map id xs === xs
 
--- prop_morally_correct :: Peano -> [Peano] -> Property
--- porp_morally_correct y xs =
---   (comp (comp reverse (map (\x -> minus x y)))
---         (comp (map (\x -> plus y x)) reverse)
---     )
---       xs
---     === id xs
+prop_morally_correct :: Peano -> [Peano] -> Property
+prop_morally_correct y xs =
+  (comp (comp reverse (map (\x -> minus x y)))
+        (comp (map (\x -> plus y x)) reverse)
+    )
+      xs
+    === id xs
diff --git a/example/CaseStudyMorallyCorrect/Output/FastLooseBasic.json b/example/CaseStudyMorallyCorrect/Output/FastLooseBasic.json
index 34393eff..c60f8cd0 100644
--- a/example/CaseStudyMorallyCorrect/Output/FastLooseBasic.json
+++ b/example/CaseStudyMorallyCorrect/Output/FastLooseBasic.json
@@ -11,10 +11,10 @@
         "FastLooseBasic.map",
         "FastLooseBasic.minus",
         "FastLooseBasic.plus",
-        "FastLooseBasic.porp_morally_correct",
         "FastLooseBasic.pred",
         "FastLooseBasic.prop_map_id",
         "FastLooseBasic.prop_minus_plus_inv",
+        "FastLooseBasic.prop_morally_correct",
         "FastLooseBasic.prop_rev_is_rev_inv",
         "FastLooseBasic.prop_reverse_is_reverseNaive",
         "FastLooseBasic.rev",
@@ -198,14 +198,6 @@
             "partial": false,
             "haskell-name": "FastLooseBasic.plus"
         },
-        {
-            "arity": 2,
-            "haskell-type": "FastLooseBasic.Peano -> Prelude.([]) FastLooseBasic.Peano -> Test.QuickCheck.Property",
-            "coq-name": "porp_morally_correct",
-            "needs-free-args": true,
-            "partial": false,
-            "haskell-name": "FastLooseBasic.porp_morally_correct"
-        },
         {
             "arity": 1,
             "haskell-type": "FastLooseBasic.Peano -> FastLooseBasic.Peano",
@@ -230,6 +222,14 @@
             "partial": false,
             "haskell-name": "FastLooseBasic.prop_minus_plus_inv"
         },
+        {
+            "arity": 2,
+            "haskell-type": "FastLooseBasic.Peano -> Prelude.([]) FastLooseBasic.Peano -> Test.QuickCheck.Property",
+            "coq-name": "prop_morally_correct",
+            "needs-free-args": true,
+            "partial": false,
+            "haskell-name": "FastLooseBasic.prop_morally_correct"
+        },
         {
             "arity": 1,
             "haskell-type": "Prelude.([]) a -> Test.QuickCheck.Property",
diff --git a/example/CaseStudyMorallyCorrect/Output/FastLooseBasic.v b/example/CaseStudyMorallyCorrect/Output/FastLooseBasic.v
index 2f93d65d..76920e3a 100644
--- a/example/CaseStudyMorallyCorrect/Output/FastLooseBasic.v
+++ b/example/CaseStudyMorallyCorrect/Output/FastLooseBasic.v
@@ -150,7 +150,25 @@ Definition comp (Shape : Type) (Pos : Shape -> Type) {b c a : Type} (g
    : Free Shape Pos c :=
   g >>= (fun g_0 => g_0 (f >>= (fun f_0 => f_0 a0))).
 
-Definition porp_morally_correct (Shape : Type) (Pos : Shape -> Type) (y
+Definition prop_minus_plus_inv (Shape : Type) (Pos : Shape -> Type) (x
+    : Free Shape Pos (Peano Shape Pos)) (y : Free Shape Pos (Peano Shape Pos))
+   : Free Shape Pos (Property Shape Pos) :=
+  @eqProp Shape Pos (Peano Shape Pos) (@comp Shape Pos (Peano Shape Pos) (Peano
+                                        Shape Pos) (Peano Shape Pos) (pure (fun (a0
+                                                                              : Free Shape Pos (Peano Shape Pos)) =>
+                                                                              minus Shape Pos a0 y)) (pure (fun (a1
+                                                                                                              : Free
+                                                                                                                Shape
+                                                                                                                Pos
+                                                                                                                (Peano
+                                                                                                                 Shape
+                                                                                                                 Pos)) =>
+                                                                                                              plus Shape
+                                                                                                                   Pos y
+                                                                                                                   a1))
+                                                                     x) x.
+
+Definition prop_morally_correct (Shape : Type) (Pos : Shape -> Type) (y
     : Free Shape Pos (Peano Shape Pos)) (xs
     : Free Shape Pos (List Shape Pos (Peano Shape Pos)))
    : Free Shape Pos (Property Shape Pos) :=
@@ -228,24 +246,6 @@ Definition porp_morally_correct (Shape : Type) (Pos : Shape -> Type) (y
                                                                                                         x_1)) x_0)) xs)
                                                        (@id Shape Pos (List Shape Pos (Peano Shape Pos)) xs).
 
-Definition prop_minus_plus_inv (Shape : Type) (Pos : Shape -> Type) (x
-    : Free Shape Pos (Peano Shape Pos)) (y : Free Shape Pos (Peano Shape Pos))
-   : Free Shape Pos (Property Shape Pos) :=
-  @eqProp Shape Pos (Peano Shape Pos) (@comp Shape Pos (Peano Shape Pos) (Peano
-                                        Shape Pos) (Peano Shape Pos) (pure (fun (a0
-                                                                              : Free Shape Pos (Peano Shape Pos)) =>
-                                                                              minus Shape Pos a0 y)) (pure (fun (a1
-                                                                                                              : Free
-                                                                                                                Shape
-                                                                                                                Pos
-                                                                                                                (Peano
-                                                                                                                 Shape
-                                                                                                                 Pos)) =>
-                                                                                                              plus Shape
-                                                                                                                   Pos y
-                                                                                                                   a1))
-                                                                     x) x.
-
 Section section_append_0.
 (* Constant arguments for append *)
 Variable Shape : Type.
diff --git a/example/CaseStudyMorallyCorrect/Output/Proofs.v b/example/CaseStudyMorallyCorrect/Output/Proofs.v
index fb0a1d63..d79edaf3 100644
--- a/example/CaseStudyMorallyCorrect/Output/Proofs.v
+++ b/example/CaseStudyMorallyCorrect/Output/Proofs.v
@@ -1,4 +1,3 @@
-
 From Base Require Import Test.QuickCheck.
 From Base Require Import Free.Instance.Identity.
 From Base Require Import Free.
@@ -45,7 +44,7 @@ Proof.
   induction xs as [ | fx fxs' IHfxs'] using List_Ind; intros facc.
   - reflexivity.
   - induction fxs' as [ xs' | sh pos IHpos] using Free_Ind.
-    + simplify2 IHfxs' as IH. simpl. simpl in IH. rewrite IH. 
+    + simplify2 IHfxs' as IH. simpl. simpl in IH. rewrite IH.
       rewrite IH with (facc := Cons fx Nil).
       rewrite <- append_assoc. reflexivity.
     + simpl. f_equal. extensionality x. simplify2 IHpos as IH. apply IH.
@@ -282,6 +281,10 @@ End small_helping_lemmas.
 
 Section main_proof.
 
+(*Theorem fancy_id : quickCheck (@prop_morally_correct Identity.Shape Identity.Pos).
+Proof.
+  simpl quickCheck.*)
+
 Theorem fancy_id : forall (fy : Free Identity.Shape Identity.Pos (Peano Identity.Shape Identity.Pos))
   (fxs : Free Identity.Shape Identity.Pos (List Identity.Shape Identity.Pos (Peano Identity.Shape Identity.Pos))),
   (comp (pure (comp (pure reverse) (pure (map (pure (fun x => minus x fy))))))

From 98e40e9e87dfc2ff88c5fd0f7dad9119bc068471 Mon Sep 17 00:00:00 2001
From: Johanna <jo-hanna_menzel@live.de>
Date: Fri, 10 Jul 2020 06:21:17 +0200
Subject: [PATCH 15/16] Restructure Case Study

---
 .../{Output => Proofs}/AppendProofs.v                       | 2 +-
 .../CaseStudyMorallyCorrect/{Output => Proofs}/PeanoInd.v   | 0
 example/CaseStudyMorallyCorrect/{Output => Proofs}/Proofs.v | 6 +++---
 .../CaseStudyMorallyCorrect/{Output => Proofs}/Simplify.v   | 0
 example/CaseStudyMorallyCorrect/Proofs/_CoqProject          | 3 +++
 5 files changed, 7 insertions(+), 4 deletions(-)
 rename example/CaseStudyMorallyCorrect/{Output => Proofs}/AppendProofs.v (98%)
 rename example/CaseStudyMorallyCorrect/{Output => Proofs}/PeanoInd.v (100%)
 rename example/CaseStudyMorallyCorrect/{Output => Proofs}/Proofs.v (98%)
 rename example/CaseStudyMorallyCorrect/{Output => Proofs}/Simplify.v (100%)
 create mode 100644 example/CaseStudyMorallyCorrect/Proofs/_CoqProject

diff --git a/example/CaseStudyMorallyCorrect/Output/AppendProofs.v b/example/CaseStudyMorallyCorrect/Proofs/AppendProofs.v
similarity index 98%
rename from example/CaseStudyMorallyCorrect/Output/AppendProofs.v
rename to example/CaseStudyMorallyCorrect/Proofs/AppendProofs.v
index 2fdf1219..fcb93370 100644
--- a/example/CaseStudyMorallyCorrect/Output/AppendProofs.v
+++ b/example/CaseStudyMorallyCorrect/Proofs/AppendProofs.v
@@ -1,6 +1,6 @@
 From Base Require Import Free.
 From Base Require Import Prelude.List.
-From Generated Require Import Simplify.
+From Proofs Require Import Simplify.
 From Generated Require Import FastLooseBasic.
 Require Import Coq.Logic.FunctionalExtensionality.
 
diff --git a/example/CaseStudyMorallyCorrect/Output/PeanoInd.v b/example/CaseStudyMorallyCorrect/Proofs/PeanoInd.v
similarity index 100%
rename from example/CaseStudyMorallyCorrect/Output/PeanoInd.v
rename to example/CaseStudyMorallyCorrect/Proofs/PeanoInd.v
diff --git a/example/CaseStudyMorallyCorrect/Output/Proofs.v b/example/CaseStudyMorallyCorrect/Proofs/Proofs.v
similarity index 98%
rename from example/CaseStudyMorallyCorrect/Output/Proofs.v
rename to example/CaseStudyMorallyCorrect/Proofs/Proofs.v
index d79edaf3..dc048185 100644
--- a/example/CaseStudyMorallyCorrect/Output/Proofs.v
+++ b/example/CaseStudyMorallyCorrect/Proofs/Proofs.v
@@ -3,9 +3,9 @@ From Base Require Import Free.Instance.Identity.
 From Base Require Import Free.
 From Base Require Import Prelude.List.
 From Generated Require Import FastLooseBasic.
-From Generated Require Import AppendProofs.
-From Generated Require Import Simplify.
-From Generated Require Import PeanoInd.
+From Proofs Require Import AppendProofs.
+From Proofs Require Import Simplify.
+From Proofs Require Import PeanoInd.
 Require Import Coq.Logic.FunctionalExtensionality.
 
 Set Implicit Arguments.
diff --git a/example/CaseStudyMorallyCorrect/Output/Simplify.v b/example/CaseStudyMorallyCorrect/Proofs/Simplify.v
similarity index 100%
rename from example/CaseStudyMorallyCorrect/Output/Simplify.v
rename to example/CaseStudyMorallyCorrect/Proofs/Simplify.v
diff --git a/example/CaseStudyMorallyCorrect/Proofs/_CoqProject b/example/CaseStudyMorallyCorrect/Proofs/_CoqProject
new file mode 100644
index 00000000..23686d98
--- /dev/null
+++ b/example/CaseStudyMorallyCorrect/Proofs/_CoqProject
@@ -0,0 +1,3 @@
+-R C:\Users\jo-ha\AppData\Roaming\cabal\store\ghc-8.6.5\free-compiler-0.2.0.0-fd18aa27c557ab924c542bb534a1ad41a611a6f9\share\base Base
+-R C:\Users\jo-ha\Desktop\free-compiler\example\CaseStudyMorallyCorrect\Output Generated
+-R . Proofs

From 23561e3f965020750b7336993e7a5141216696bb Mon Sep 17 00:00:00 2001
From: Johanna <jo-hanna_menzel@live.de>
Date: Wed, 15 Jul 2020 17:10:05 +0200
Subject: [PATCH 16/16] Add Readme and restructure case study

---
 .../AppendProofs.v                            |  0
 .../PeanoInd.v                                |  0
 .../Simplify.v                                |  0
 .../{Proofs => }/Proofs.v                     |  0
 .../Proofs/_CoqProject                        |  3 ---
 example/CaseStudyMorallyCorrect/README.md     | 22 +++++++++++++++++++
 6 files changed, 22 insertions(+), 3 deletions(-)
 rename example/CaseStudyMorallyCorrect/{Proofs => ProofInfrastructure}/AppendProofs.v (100%)
 rename example/CaseStudyMorallyCorrect/{Proofs => ProofInfrastructure}/PeanoInd.v (100%)
 rename example/CaseStudyMorallyCorrect/{Proofs => ProofInfrastructure}/Simplify.v (100%)
 rename example/CaseStudyMorallyCorrect/{Proofs => }/Proofs.v (100%)
 delete mode 100644 example/CaseStudyMorallyCorrect/Proofs/_CoqProject
 create mode 100644 example/CaseStudyMorallyCorrect/README.md

diff --git a/example/CaseStudyMorallyCorrect/Proofs/AppendProofs.v b/example/CaseStudyMorallyCorrect/ProofInfrastructure/AppendProofs.v
similarity index 100%
rename from example/CaseStudyMorallyCorrect/Proofs/AppendProofs.v
rename to example/CaseStudyMorallyCorrect/ProofInfrastructure/AppendProofs.v
diff --git a/example/CaseStudyMorallyCorrect/Proofs/PeanoInd.v b/example/CaseStudyMorallyCorrect/ProofInfrastructure/PeanoInd.v
similarity index 100%
rename from example/CaseStudyMorallyCorrect/Proofs/PeanoInd.v
rename to example/CaseStudyMorallyCorrect/ProofInfrastructure/PeanoInd.v
diff --git a/example/CaseStudyMorallyCorrect/Proofs/Simplify.v b/example/CaseStudyMorallyCorrect/ProofInfrastructure/Simplify.v
similarity index 100%
rename from example/CaseStudyMorallyCorrect/Proofs/Simplify.v
rename to example/CaseStudyMorallyCorrect/ProofInfrastructure/Simplify.v
diff --git a/example/CaseStudyMorallyCorrect/Proofs/Proofs.v b/example/CaseStudyMorallyCorrect/Proofs.v
similarity index 100%
rename from example/CaseStudyMorallyCorrect/Proofs/Proofs.v
rename to example/CaseStudyMorallyCorrect/Proofs.v
diff --git a/example/CaseStudyMorallyCorrect/Proofs/_CoqProject b/example/CaseStudyMorallyCorrect/Proofs/_CoqProject
deleted file mode 100644
index 23686d98..00000000
--- a/example/CaseStudyMorallyCorrect/Proofs/_CoqProject
+++ /dev/null
@@ -1,3 +0,0 @@
--R C:\Users\jo-ha\AppData\Roaming\cabal\store\ghc-8.6.5\free-compiler-0.2.0.0-fd18aa27c557ab924c542bb534a1ad41a611a6f9\share\base Base
--R C:\Users\jo-ha\Desktop\free-compiler\example\CaseStudyMorallyCorrect\Output Generated
--R . Proofs
diff --git a/example/CaseStudyMorallyCorrect/README.md b/example/CaseStudyMorallyCorrect/README.md
new file mode 100644
index 00000000..9001b8fa
--- /dev/null
+++ b/example/CaseStudyMorallyCorrect/README.md
@@ -0,0 +1,22 @@
+| Compile haskell source files |      |                                                              |
+| ---------------------------- | ---- | ------------------------------------------------------------ |
+|                              |      |                                                              |
+|                              |      | You need to compile the haskell source file with the free-compiler and put the result into the `../Output` folder. |
+|                              |      | The source file is `FastAndLooseReasoning.hs`                |
+|                              |      | If you are in the root directory of the free-compiler you can run the following command for the compilation process. |
+|                              |      |                                                              |
+|                              |      | ```                                                          |
+|                              |      | cabal new-run freec -- --transform-pattern-matching -o example/CaseStudyMorallyCorrect/Output example/CaseStudyMorallyCorrect/FastAndLooseReasoning.hs |
+|                              |      | ```                                                          |
+|                              |      |                                                              |
+| **Compile Coq files**        |      |                                                              |
+|                              |      |                                                              |
+|                              |      | To run the proof file `Proof.v` you need to compile the dependencies first. |
+|                              |      | Make sure that your `_CoqProject` is locted in `CaseStudyMorallyCorrect` and not in one of its subdirectories.  Add the following lines into the `_CoqProject`<br /> `-R .\Output Generated` <br/>`-R .\ProofInfrastructure Proofs` |
+|                              |      | The easiest way to do so is to create a `Makefile` from the `_CoqProject` in this directory and run it. |
+|                              |      | ```                                                          |
+|                              |      | coq_makefile -f _CoqProject -o Makefile                      |
+|                              |      | make                                                         |
+|                              |      | ```                                                          |
+|                              |      | The easiest way to do so is to create a `Makefile` from the `_CoqProject` in this directory and run it. |
+|                              |      | The `Proof.v` file can now be executed.                      |
\ No newline at end of file