X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskStrongToProof.v;h=1f1229d66651b2a6d24a74fac77524b85242fdd0;hp=8a49c81fe11368099b5e6acb29941aa2c68685b2;hb=af41ffb1692ae207554342ccdc3bf73abaa75a01;hpb=9241d797587022ecd51e3c38cd34588de6745524 diff --git a/src/HaskStrongToProof.v b/src/HaskStrongToProof.v index 8a49c81..1f1229d 100644 --- a/src/HaskStrongToProof.v +++ b/src/HaskStrongToProof.v @@ -6,6 +6,7 @@ Generalizable All Variables. Require Import Preamble. Require Import General. Require Import NaturalDeduction. +Require Import NaturalDeductionContext. Require Import Coq.Strings.String. Require Import Coq.Lists.List. Require Import Coq.Init.Specif. @@ -15,20 +16,7 @@ Require Import HaskStrong. Require Import HaskProof. Section HaskStrongToProof. - -Definition pivotContext {T} a b c : @Arrange T ((a,,b),,c) ((a,,c),,b) := - RComp (RComp (RCossa _ _ _) (RLeft a (RExch c b))) (RAssoc _ _ _). - -Definition pivotContext' {T} a b c : @Arrange T (a,,(b,,c)) (b,,(a,,c)) := - RComp (RComp (RAssoc _ _ _) (RRight c (RExch b a))) (RCossa _ _ _). - -Definition copyAndPivotContext {T} a b c : @Arrange T ((a,,b),,(c,,b)) ((a,,c),,b). - eapply RComp; [ idtac | apply (RLeft (a,,c) (RCont b)) ]. - eapply RComp; [ idtac | apply RCossa ]. - eapply RComp; [ idtac | apply (RRight b (pivotContext a b c)) ]. - apply RAssoc. - Defined. - + Context {VV:Type}{eqd_vv:EqDecidable VV}. (* maintenance of Xi *) @@ -633,16 +621,16 @@ Definition factorContextLeft (* where the leaf is v *) apply inr. subst. - apply RuCanR. + apply AuCanR. (* where the leaf is NOT v *) apply inl. - apply RuCanL. + apply AuCanL. (* empty leaf *) destruct case_None. apply inl; simpl in *. - apply RuCanR. + apply AuCanR. (* branch *) refine ( @@ -662,45 +650,45 @@ Definition factorContextLeft destruct case_Neither. apply inl. simpl. - eapply RComp; [idtac | apply RuCanL ]. - exact (RComp + eapply AComp; [idtac | apply AuCanL ]. + exact (AComp (* order will not matter because these are central as morphisms *) - (RRight _ (RComp lpf (RCanL _))) - (RLeft _ (RComp rpf (RCanL _)))). + (ARight _ (AComp lpf (ACanL _))) + (ALeft _ (AComp rpf (ACanL _)))). destruct case_Right. apply inr. unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *. fold (stripOutVars (v::nil)). - eapply RComp; [ idtac | eapply pivotContext' ]. - eapply RComp. - eapply RRight. - eapply RComp. + eapply AComp; [ idtac | eapply pivotContext' ]. + eapply AComp. + eapply ARight. + eapply AComp. apply lpf. - apply RCanL. - eapply RLeft. + apply ACanL. + eapply ALeft. apply rpf. destruct case_Left. apply inr. fold (stripOutVars (v::nil)). simpl. - eapply RComp. - eapply RLeft. - eapply RComp. + eapply AComp. + eapply ALeft. + eapply AComp. apply rpf. simpl. - eapply RCanL. - eapply RComp; [ idtac | eapply RCossa ]. - eapply RRight. + eapply ACanL. + eapply AComp; [ idtac | eapply AuAssoc ]. + eapply ARight. apply lpf. destruct case_Both. apply inr. simpl. - eapply RComp; [ idtac | eapply RRight; eapply RCont ]. - eapply RComp; [ eapply RRight; eapply lpf | idtac ]. - eapply RComp; [ eapply RLeft; eapply rpf | idtac ]. + eapply AComp; [ idtac | eapply ARight; eapply ACont ]. + eapply AComp; [ eapply ARight; eapply lpf | idtac ]. + eapply AComp; [ eapply ALeft; eapply rpf | idtac ]. clear lpf rpf. simpl. apply arrangeSwapMiddle. @@ -738,16 +726,16 @@ Definition factorContextRight (* where the leaf is v *) apply inr. subst. - apply RuCanL. + apply AuCanL. (* where the leaf is NOT v *) apply inl. - apply RuCanR. + apply AuCanR. (* empty leaf *) destruct case_None. apply inl; simpl in *. - apply RuCanR. + apply AuCanR. (* branch *) refine ( @@ -766,51 +754,51 @@ Definition factorContextRight destruct case_Neither. apply inl. - eapply RComp; [idtac | apply RuCanR ]. - exact (RComp + eapply AComp; [idtac | apply AuCanR ]. + exact (AComp (* order will not matter because these are central as morphisms *) - (RRight _ (RComp lpf (RCanR _))) - (RLeft _ (RComp rpf (RCanR _)))). + (ARight _ (AComp lpf (ACanR _))) + (ALeft _ (AComp rpf (ACanR _)))). destruct case_Right. apply inr. fold (stripOutVars (v::nil)). - set (RRight (mapOptionTree ξ ctx2) (RComp lpf ((RCanR _)))) as q. + set (ARight (mapOptionTree ξ ctx2) (AComp lpf ((ACanR _)))) as q. simpl in *. - eapply RComp. + eapply AComp. apply q. clear q. clear lpf. unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *. - eapply RComp; [ idtac | apply RAssoc ]. - apply RLeft. + eapply AComp; [ idtac | apply AAssoc ]. + apply ALeft. apply rpf. destruct case_Left. apply inr. unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *. fold (stripOutVars (v::nil)). - eapply RComp; [ idtac | eapply pivotContext ]. - set (RComp rpf (RCanR _ )) as rpf'. - set (RLeft ((mapOptionTree ξ (stripOutVars (v :: nil) ctx1),, [ξ v])) rpf') as qq. + eapply AComp; [ idtac | eapply pivotContext ]. + set (AComp rpf (ACanR _ )) as rpf'. + set (ALeft ((mapOptionTree ξ (stripOutVars (v :: nil) ctx1),, [ξ v])) rpf') as qq. simpl in *. - eapply RComp; [ idtac | apply qq ]. + eapply AComp; [ idtac | apply qq ]. clear qq rpf' rpf. - apply (RRight (mapOptionTree ξ ctx2)). + apply (ARight (mapOptionTree ξ ctx2)). apply lpf. destruct case_Both. apply inr. unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *. fold (stripOutVars (v::nil)). - eapply RComp; [ idtac | eapply copyAndPivotContext ]. + eapply AComp; [ idtac | eapply copyAndPivotContext ]. (* order will not matter because these are central as morphisms *) - exact (RComp (RRight _ lpf) (RLeft _ rpf)). + exact (AComp (ARight _ lpf) (ALeft _ rpf)). Defined. -(* same as before, but use RWeak if necessary *) +(* same as before, but use AWeak if necessary *) Definition factorContextLeftAndWeaken (Γ:TypeEnv)(Δ:CoercionEnv Γ) v (* variable to be pivoted, if found *) @@ -821,8 +809,8 @@ Definition factorContextLeftAndWeaken (mapOptionTree ξ ([v],,(stripOutVars (v::nil) ctx)) ). set (factorContextLeft Γ Δ v ctx ξ) as q. destruct q; auto. - eapply RComp; [ apply a | idtac ]. - refine (RRight _ (RWeak _)). + eapply AComp; [ apply a | idtac ]. + refine (ARight _ (AWeak _)). Defined. Definition factorContextLeftAndWeaken'' @@ -848,7 +836,7 @@ Definition factorContextLeftAndWeaken'' unfold mapOptionTree; simpl in *. intros. rewrite (@stripping_nothing_is_inert Γ); auto. - apply RuCanL. + apply AuCanL. intros. unfold mapOptionTree in *. simpl in *. @@ -867,15 +855,15 @@ Definition factorContextLeftAndWeaken'' unfold stripOutVars in q. rewrite q in IHv1'. clear q. - eapply RComp; [ idtac | eapply RAssoc ]. - eapply RComp; [ idtac | eapply IHv1' ]. + eapply AComp; [ idtac | eapply AAssoc ]. + eapply AComp; [ idtac | eapply IHv1' ]. clear IHv1'. apply IHv2; auto. auto. auto. Defined. -(* same as before, but use RWeak if necessary *) +(* same as before, but use AWeak if necessary *) Definition factorContextRightAndWeaken (Γ:TypeEnv)(Δ:CoercionEnv Γ) v (* variable to be pivoted, if found *) @@ -886,8 +874,8 @@ Definition factorContextRightAndWeaken (mapOptionTree ξ ((stripOutVars (v::nil) ctx),,[v]) ). set (factorContextRight Γ Δ v ctx ξ) as q. destruct q; auto. - eapply RComp; [ apply a | idtac ]. - refine (RLeft _ (RWeak _)). + eapply AComp; [ apply a | idtac ]. + refine (ALeft _ (AWeak _)). Defined. Definition factorContextRightAndWeaken'' @@ -911,7 +899,7 @@ Definition factorContextRightAndWeaken'' unfold mapOptionTree; simpl in *. intros. rewrite (@stripping_nothing_is_inert Γ); auto. - apply RuCanR. + apply AuCanR. intros. unfold mapOptionTree in *. simpl in *. @@ -930,14 +918,14 @@ Definition factorContextRightAndWeaken'' fold X in IHv2'. set (distinct_app _ _ _ H) as H'. destruct H' as [H1 H2]. - set (RComp (IHv1 _ H1) (IHv2' H2)) as qq. - eapply RComp. + set (AComp (IHv1 _ H1) (IHv2' H2)) as qq. + eapply AComp. apply qq. clear qq IHv2' IHv2 IHv1. rewrite strip_swap_lemma. rewrite strip_twice_lemma. rewrite (notin_strip_inert' v1 (leaves v2)). - apply RCossa. + apply AuAssoc. apply distinct_swap. auto. Defined. @@ -973,10 +961,13 @@ Lemma letRecSubproofsToND Γ Δ ξ lev tree branches : destruct q. simpl in *. apply n. - eapply nd_comp; [ idtac | eapply nd_rule; apply RJoin ]. - eapply nd_comp; [ apply nd_llecnac | idtac ]. - apply nd_prod; auto. - Defined. + eapply nd_comp; [ idtac | eapply RCut' ]. + eapply nd_comp; [ apply nd_llecnac | idtac ]. + apply nd_prod. + apply IHX1. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RLeft ]. + apply IHX2. + Defined. Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree : forall branches body (dist:distinct (leaves (mapOptionTree (@fst _ _) tree))), @@ -1027,10 +1018,14 @@ Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree : simpl. set (letRecSubproofsToND _ _ _ _ _ branches lrsp) as q. - eapply nd_comp; [ idtac | eapply nd_rule; apply RJoin ]. - eapply nd_comp; [ apply nd_rlecnac | idtac ]. - apply nd_prod; auto. - Defined. + + eapply nd_comp; [ idtac | eapply RCut' ]. + eapply nd_comp; [ apply nd_llecnac | idtac ]. + apply nd_prod. + apply q. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RLeft ]. + apply pf. + Defined. Lemma scbwv_coherent {tc}{Γ}{atypes:IList _ (HaskType Γ) _}{sac} : forall scb:StrongCaseBranchWithVVs _ _ tc atypes sac, @@ -1194,7 +1189,7 @@ Definition expr2proof : inversion H. destruct case_ELet; intros; simpl in *. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ]. + eapply nd_comp; [ idtac | eapply RLet ]. eapply nd_comp; [ apply nd_rlecnac | idtac ]. apply nd_prod. apply pf_let.