Use custom simpl lemmas in Case Study Morally Correct

example/CaseStudyMorallyCorrect/Proofs/AppendProofs.v → example/CaseStudyMorallyCorrect/ProofInfrastructure/AppendProofs.v

@@ -1,6 +1,7 @@
 From Base Require Import Free.
 From Base Require Import Prelude.List.
 From Proofs Require Import Simplify.
+From Proofs Require Import SimplLemmas.
 From Generated Require Import FastLooseBasic.
 Require Import Coq.Logic.FunctionalExtensionality.
 
@@ -10,10 +11,16 @@ Arguments append {_} {_} {_} _ _.
 Arguments Nil {_} {_} {_}.
 Arguments Cons {_} {_} {_} _ _.
 
+Opaque Nil.
+Opaque 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.
+  intros.
+  rewrite apply_append_cons.
+  rewrite apply_append_nil.
   reflexivity.
 Qed. 
 
@@ -24,10 +31,9 @@ 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.
+  - induction fxs as [ xs | s pf IHpf ] using Free_Ind; rewrite cons_Cons; do 3 rewrite apply_append_cons; f_equal. 
+    + simplify H as IH'. apply IH'.
+    + simpl. f_equal. extensionality x. simplify2 IHimp as IH. apply IH.
 Qed.
 
 Lemma append_assoc : forall (Shape : Type) (Pos : Shape -> Type) (A : Type)
@@ -49,10 +55,9 @@ Proof.
   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.
+    - induction fxs' as [ xs' | s pf IHpf ] using Free_Ind; rewrite cons_Cons; rewrite apply_append_cons; f_equal.
+      * simplify IHfxs' as IH. apply IH.
+      * simpl. f_equal. extensionality x. simplify2 IHfxs' as IH. apply IH.
   + simpl. f_equal. extensionality x. apply IHpf.
 Qed.
 

example/CaseStudyMorallyCorrect/ProofInfrastructure/SimplLemmas.v

@@ -0,0 +1,94 @@
+From Base Require Import Free.
+From Base Require Import Prelude.List.
+From Generated Require Import FastLooseBasic.
+
+Arguments Nil {_} {_} {_}.
+Arguments Cons {_} {_} {_} _ _.
+Arguments S {_} {_} _.
+Arguments Zero {_} {_}.
+Arguments append {_} {_} {_} _ _.
+Arguments rev {_} {_} {_} _ _.
+Arguments reverse {_} {_} {_} _ .
+Arguments reverseNaive {_} {_} {_} _ .
+Arguments plus {_} {_} _ _.
+Arguments minus {_} {_} _ _.
+Arguments pred {_} {_} _.
+Arguments map {_} {_} {_} {_} _ _.
+Arguments foldPeano {_} {_} {_} _ _ _.
+
+Lemma cons_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) = Cons fx fxs.
+Proof.
+  reflexivity.
+Qed.
+
+Lemma nil_Nil: forall (Shape : Type) (Pos : Shape -> Type) (A : Type),
+  pure (@nil Shape Pos A) = Nil.
+Proof.
+  reflexivity.
+Qed.
+
+Lemma apply_append_nil: forall (Shape : Type) (Pos : Shape -> Type) (A : Type)
+  (fxs : Free Shape Pos (List Shape Pos A)),
+  append Nil fxs = fxs.
+Proof.
+  reflexivity.
+Qed.
+
+Lemma apply_append_cons: forall (Shape : Type) (Pos : Shape -> Type) (A : Type)
+  (fx : Free Shape Pos A) ( fxs fys : Free Shape Pos (List Shape Pos A)),
+  append (Cons fx fxs) fys = Cons fx (append fxs fys).
+Proof.
+  reflexivity.
+Qed.
+
+Lemma apply_reverseNaive: forall (Shape : Type) (Pos : Shape -> Type) (A : Type)
+  (fx : Free Shape Pos A) (fxs : Free Shape Pos (List Shape Pos A)),
+  reverseNaive (Cons fx fxs) =  append (reverseNaive fxs) (Cons fx Nil).
+Proof.
+  reflexivity.
+Qed.
+
+Lemma apply_rev: forall (Shape : Type) (Pos : Shape -> Type) (A : Type)
+  (fx : Free Shape Pos A) (fxs fys: Free Shape Pos (List Shape Pos A)),
+  rev (Cons fx fxs) fys = rev fxs (Cons fx fys).
+Proof.
+  reflexivity.
+Qed.
+
+Lemma apply_map: forall (Shape : Type) (Pos : Shape -> Type) (A B : Type)
+  (fx : Free Shape Pos A) (fxs : Free Shape Pos (List Shape Pos A)) 
+  (ff : Free Shape Pos (Free Shape Pos A -> Free Shape Pos B)),
+  map ff (Cons fx fxs) = Cons (ff >>= (fun f => f fx)) (map ff fxs).
+Proof.
+  reflexivity.
+Qed.
+
+Lemma s_S: forall (Shape : Type) (Pos : Shape -> Type) (fn : Free Shape Pos (Peano Shape Pos)),
+  pure (s fn) = S fn.
+Proof.
+  reflexivity.
+Qed.
+
+Lemma zero_Zero: forall (Shape : Type) (Pos : Shape -> Type),
+  pure (@zero Shape Pos) = Zero.
+Proof.
+  reflexivity.
+Qed.
+
+Lemma apply_pred: forall (Shape : Type) (Pos : Shape -> Type) (fn : Free Shape Pos (Peano Shape Pos)),
+  pred (S fn) = fn. 
+Proof.
+  reflexivity.
+Qed.
+
+Lemma apply_foldPeano: forall (Shape : Type) (Pos : Shape -> Type) (A : Type) 
+  (f : Free Shape Pos A -> Free Shape Pos A) (fa : Free Shape Pos A) (fn : Free Shape Pos (Peano Shape Pos)),
+  foldPeano (pure f) fa (S fn) = f (foldPeano (pure f) fa fn).
+Proof.
+  reflexivity.
+Qed.
+
+
+

example/CaseStudyMorallyCorrect/Proofs/Proofs.v → example/CaseStudyMorallyCorrect/Proofs.v

@@ -6,6 +6,7 @@ From Generated Require Import FastLooseBasic.
 From Proofs Require Import AppendProofs.
 From Proofs Require Import Simplify.
 From Proofs Require Import PeanoInd.
+From Proofs Require Import SimplLemmas.
 Require Import Coq.Logic.FunctionalExtensionality.
 
 Set Implicit Arguments.
@@ -29,22 +30,15 @@ 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.
+  - induction fxs' as [ xs' | sh pos IHpos] using Free_Ind; rewrite cons_Cons; unfold reverse; do 2 rewrite apply_rev. 
+    + simplify2 IHfxs' as 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.
@@ -67,9 +61,8 @@ 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.
+  - induction fxs' as [ xs' | sh pos IHpos ] using Free_Ind; rewrite cons_Cons; unfold reverse; rewrite apply_reverseNaive; rewrite apply_rev.
+    + simplify IHfxs' as IH.
       rewrite rev_acc_and_rest_list_connection. rewrite IH. reflexivity.
     + simpl. f_equal. extensionality x. simplify2 IHpos as IH. apply IH.
 Qed.
@@ -88,13 +81,6 @@ 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).
@@ -104,8 +90,9 @@ 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 cons_Cons. rewrite apply_reverseNaive. 
       rewrite append_assoc.
+      simplify2 IHfxs' as IHxs'.
       rewrite <- IHxs'. reflexivity.
 Qed.
 
@@ -118,8 +105,8 @@ Proof.
   - 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.
+      * rewrite cons_Cons. rewrite apply_reverseNaive. rewrite reverseNaive_append. 
+        simplify2 IHfxs' as IHxs'. rewrite IHxs'. reflexivity.
 Qed.
 
 Theorem reverse_is_involution: quickCheck (@prop_rev_is_rev_inv Identity.Shape Identity.Pos).
@@ -136,21 +123,20 @@ 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).
+  plus 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.
+  - induction fx' as [ x' | sh pos IHpos ] using Free_Ind; rewrite s_S; unfold plus; rewrite apply_foldPeano; f_equal.
+    + simplify2 IHfx' as IH. apply IH.
+    + simpl. 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.
+  plus Zero fx = fx.
 Proof.
   intros Shape Pos fx.
   induction fx as [ x | pf sh IHpos ] using Free_Ind.
@@ -159,34 +145,35 @@ Proof.
 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)).
+  plus (S fy) fx = 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.
+  - destruct fx' as [ x' | [] _ ]; rewrite s_S.
+    + simplify2 IHfx' as IH. unfold plus. rewrite apply_foldPeano. f_equal.
+      simpl. apply IH. 
 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.
+  minus fx (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.
+    + induction fy' as [ y' | sh pos IHpos ] using Free_Ind; 
+      rewrite s_S; unfold minus; rewrite apply_foldPeano; simpl; f_equal.
+      * simplify2 IHfy' as IH. apply IH.
+      * 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.
+   pred (S fx) = fx.
 Proof.
   intros Shape Pos fx.
   destruct fx as [ x | sh pf ].
@@ -204,7 +191,7 @@ Proof.
   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.
+    + rewrite s_S. 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)),
@@ -229,6 +216,7 @@ Proof.
   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)),
@@ -239,8 +227,9 @@ Proof.
   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.
+    + induction fxs' as [ xs' | sh pos IHpos ] using Free_Ind; rewrite cons_Cons.
+      * simpl. f_equal.
+        simplify2 IHfxs as IH. apply IH.
       * simpl. do 2 f_equal. extensionality x. simplify2 IHpos as IH. apply IH.
   - simpl. f_equal. extensionality x. apply IHpos.
 Qed.
@@ -253,9 +242,10 @@ Proof.
   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.
+    + induction fxs' as [ xs' | sh pos IHpos ] using Free_Ind;
+      rewrite cons_Cons; rewrite apply_map; f_equal. 
+      * simplify2 IHfxs as IH. apply IH.
+      * simpl. f_equal. extensionality x. simplify2 IHpos as IH. apply IH.
   - simpl. f_equal. extensionality x. apply IHpos.
 Qed.
 
@@ -281,23 +271,19 @@ End small_helping_lemmas.
 
 Section main_proof.
 
-(*Theorem fancy_id : quickCheck (@prop_morally_correct Identity.Shape Identity.Pos).
-Proof.
-  simpl quickCheck.*)
+Opaque comp.
 
-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.
+Theorem fancy_id : quickCheck (@prop_morally_correct Identity.Shape Identity.Pos).
 Proof.
+  simpl quickCheck.
   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.
+Transparent comp.
   simpl. 
   apply reverse_is_involution.
 Qed.