diff --git a/example/CaseStudyMorallyCorrect/Proofs/AppendProofs.v b/example/CaseStudyMorallyCorrect/ProofInfrastructure/AppendProofs.v similarity index 72% rename from example/CaseStudyMorallyCorrect/Proofs/AppendProofs.v rename to example/CaseStudyMorallyCorrect/ProofInfrastructure/AppendProofs.v index fcb93370..5e955e93 100644 --- a/example/CaseStudyMorallyCorrect/Proofs/AppendProofs.v +++ b/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. 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/ProofInfrastructure/SimplLemmas.v b/example/CaseStudyMorallyCorrect/ProofInfrastructure/SimplLemmas.v new file mode 100644 index 00000000..85aaba52 --- /dev/null +++ b/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. + + + 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 75% rename from example/CaseStudyMorallyCorrect/Proofs/Proofs.v rename to example/CaseStudyMorallyCorrect/Proofs.v index dc048185..9aff62cd 100644 --- a/example/CaseStudyMorallyCorrect/Proofs/Proofs.v +++ b/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,13 +30,6 @@ 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. @@ -43,8 +37,8 @@ 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,16 +271,11 @@ 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)))). @@ -298,6 +283,7 @@ Proof. rewrite minus_plus_inv. rewrite map_id. rewrite comp_id. +Transparent comp. simpl. apply reverse_is_involution. Qed. 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