diff --git a/example/CaseStudyMorallyCorrect/FastAndLooseReasoning.hs b/example/CaseStudyMorallyCorrect/FastAndLooseReasoning.hs
new file mode 100644
index 00000000..3bed1a85
--- /dev/null
+++ b/example/CaseStudyMorallyCorrect/FastAndLooseReasoning.hs
@@ -0,0 +1,63 @@
+module FastLooseBasic where
+
+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 []
+
+rev [] acc = acc
+rev (x : xs) acc = rev xs (x : acc)
+
+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_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
+
+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
+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
new file mode 100644
index 00000000..c60f8cd0
--- /dev/null
+++ b/example/CaseStudyMorallyCorrect/Output/FastLooseBasic.json
@@ -0,0 +1,426 @@
+{
+ "type-synonyms": [],
+ "library-name": "Generated",
+ "exported-values": [
+ "FastLooseBasic.S",
+ "FastLooseBasic.Zero",
+ "FastLooseBasic.append",
+ "FastLooseBasic.comp",
+ "FastLooseBasic.foldPeano",
+ "FastLooseBasic.id",
+ "FastLooseBasic.map",
+ "FastLooseBasic.minus",
+ "FastLooseBasic.plus",
+ "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",
+ "FastLooseBasic.reverse",
+ "FastLooseBasic.reverseNaive"
+ ],
+ "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": 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",
+ "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_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_plus_inv",
+ "needs-free-args": true,
+ "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",
+ "coq-name": "prop_rev_is_rev_inv",
+ "needs-free-args": true,
+ "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",
+ "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.([]) 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",
+ "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..76920e3a
--- /dev/null
+++ b/example/CaseStudyMorallyCorrect/Output/FastLooseBasic.v
@@ -0,0 +1,296 @@
+(* 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} (a15
+ : List Shape Pos t0) (a16 : Free Shape Pos (List Shape Pos t0)) {struct a15}
+ : Free Shape Pos (List Shape Pos t0)
+ := 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} (a15
+ : Free Shape Pos (List Shape Pos t0)) (a16
+ : Free Shape Pos (List Shape Pos t0))
+ : Free Shape Pos (List Shape Pos t0) :=
+ 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))
+ : Free Shape Pos (List Shape Pos a) :=
+ @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))
+ : 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) (a27
+ : Free Shape Pos (Peano Shape Pos))
+ : Free Shape Pos (Peano Shape Pos) :=
+ 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 a21_0 : Free Shape Pos (Free Shape Pos a_0 -> Free Shape Pos b_0).
+(* Helper functions for map *)
+Fixpoint map_1 (a22 : List Shape Pos a_0) {struct a22} : Free Shape Pos (List
+ Shape Pos b_0)
+ := match a22 with
+ | nil => @Nil Shape Pos b_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 (a22 : Free Shape Pos (List Shape Pos a_0))
+ : Free Shape Pos (List Shape Pos b_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} (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 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 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 (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 (a32 : Free Shape Pos (Peano Shape Pos))
+ : Free Shape Pos a_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} (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 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))
+ : 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))).
+
+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) :=
+ @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).
+
+Section section_append_0.
+(* Constant arguments for append *)
+Variable Shape : Type.
+Variable Pos : Shape -> Type.
+Variable a_0 : Type.
+Variable a5_0 : Free Shape Pos (List Shape Pos a_0).
+(* Helper functions for append *)
+Fixpoint append_1 (a4 : List Shape Pos a_0) {struct a4} : Free Shape Pos (List
+ Shape Pos a_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 (a4 : Free Shape Pos (List Shape Pos a_0))
+ : Free Shape Pos (List Shape Pos a_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} (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 a5 a4.
+
+(* Helper functions for reverseNaive *)
+
+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 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} (a10
+ : Free Shape Pos (List Shape Pos a))
+ : Free Shape Pos (List Shape Pos a) :=
+ 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))
+ : 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/ProofInfrastructure/AppendProofs.v b/example/CaseStudyMorallyCorrect/ProofInfrastructure/AppendProofs.v
new file mode 100644
index 00000000..fcb93370
--- /dev/null
+++ b/example/CaseStudyMorallyCorrect/ProofInfrastructure/AppendProofs.v
@@ -0,0 +1,61 @@
+From Base Require Import Free.
+From Base Require Import Prelude.List.
+From Proofs 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 IHimp ] 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. 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)),
+ 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 = fxs.
+Proof.
+ 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.
+
+
+
+
diff --git a/example/CaseStudyMorallyCorrect/ProofInfrastructure/PeanoInd.v b/example/CaseStudyMorallyCorrect/ProofInfrastructure/PeanoInd.v
new file mode 100644
index 00000000..725ea498
--- /dev/null
+++ b/example/CaseStudyMorallyCorrect/ProofInfrastructure/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/ProofInfrastructure/Simplify.v b/example/CaseStudyMorallyCorrect/ProofInfrastructure/Simplify.v
new file mode 100644
index 00000000..d4e715cb
--- /dev/null
+++ b/example/CaseStudyMorallyCorrect/ProofInfrastructure/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).
diff --git a/example/CaseStudyMorallyCorrect/Proofs.v b/example/CaseStudyMorallyCorrect/Proofs.v
new file mode 100644
index 00000000..dc048185
--- /dev/null
+++ b/example/CaseStudyMorallyCorrect/Proofs.v
@@ -0,0 +1,305 @@
+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.
+From Proofs Require Import AppendProofs.
+From Proofs Require Import Simplify.
+From Proofs Require Import PeanoInd.
+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 {_} {_} {_} _ _.
+Arguments plus {_} {_} _ _.
+Arguments minus {_} {_} _ _.
+Arguments pred {_} {_} _.
+Arguments map {_} {_} {_} {_} _ _.
+Arguments comp {_} {_} {_} {_} {_} _ _.
+Arguments id {_} {_} {_} _.
+Arguments S {_} {_} _.
+Arguments Zero {_} {_}.
+
+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.
+Proof.
+ intros Shape Pos A xs.
+ 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.
+ rewrite IH with (facc := Cons fx Nil).
+ rewrite <- append_assoc. reflexivity.
+ + 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)
+ (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 IHpos ] using Free_Ind.
+ - apply rev_acc_and_rest_list_connection'.
+ - simpl. f_equal. extensionality x. apply IHpos.
+Qed.
+
+Lemma reverse_is_reverseNaive': forall (Shape : Type) (Pos : Shape -> Type) (A : Type)
+ (xs : List Shape Pos A),
+ reverse (pure xs) = reverseNaive (pure xs).
+Proof.
+ intros Shape Pos A xs.
+ induction xs as [ | fx fxs' IHfxs' ] using List_Ind.
+ - reflexivity.
+ - 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 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 IHpos ] using Free_Ind.
+ - apply reverse_is_reverseNaive'.
+ - simpl. f_equal. extensionality x. apply IHpos.
+Qed.
+
+End reverseIsReverseNaive.
+
+
+Section reverse_is_involution.
+
+Lemma reverseNaive_0_reverseNaive: forall (Shape : Type) (Pos : Shape -> Type) (A : Type)
+ (xs : List Shape Pos A),
+ reverseNaive_0 xs = reverseNaive (pure xs).
+Proof.
+ 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.
+ + 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.
+
+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' IHfx' ] using Peano_Ind.
+ - reflexivity.
+ - 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 IHpos 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 IHpos ] using Free_Ind.
+ - apply plus_zero'.
+ - simpl. f_equal. extensionality x. apply IHpos.
+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.
+ intros fx fy.
+ destruct fx as [ x | [] _ ].
+ 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 IHpos ] using Free_Ind.
+ - induction y as [ | fy' IHfy' ] using Peano_Ind.
+ + reflexivity.
+ + 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 IHpos as IH. apply IH.
+ - simpl. f_equal. extensionality x. apply IHpos.
+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_ext: quickCheck (@prop_minus_plus_inv Identity.Shape Identity.Pos).
+Proof.
+ simpl quickCheck.
+ 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.
+
+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 : 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))))))
+ (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
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`
`-R .\Output Generated`
`-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