X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskProofToStrong.v;h=299a83be3703e2cded3a29e49bbeafc697dca2d4;hp=78c2e41bde6311e7b9430c19e0d8ad657ac87f76;hb=1a2754d2e135ef3c5fd7ef817e1129af93b533a5;hpb=57e387249da84dac0f1c5a9411e3900831ce2d81 diff --git a/src/HaskProofToStrong.v b/src/HaskProofToStrong.v index 78c2e41..299a83b 100644 --- a/src/HaskProofToStrong.v +++ b/src/HaskProofToStrong.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. @@ -28,10 +29,10 @@ Section HaskProofToStrong. Definition judg2exprType (j:Judg) : Type := match j with (Γ > Δ > Σ |- τ @ l) => forall (ξ:ExprVarResolver Γ) vars, Σ = mapOptionTree ξ vars -> - FreshM (ITree _ (fun t => Expr Γ Δ ξ (t @@ l)) τ) + FreshM (ITree _ (fun t => Expr Γ Δ ξ t l) τ) end. - Definition justOne Γ Δ ξ τ : ITree _ (fun t => Expr Γ Δ ξ t) [τ] -> Expr Γ Δ ξ τ. + Definition justOne Γ Δ ξ τ l : ITree _ (fun t => Expr Γ Δ ξ t l) [τ] -> Expr Γ Δ ξ τ l. intros. inversion X; auto. Defined. @@ -223,7 +224,7 @@ Section HaskProofToStrong. Defined. Definition ujudg2exprType Γ (ξ:ExprVarResolver Γ)(Δ:CoercionEnv Γ) Σ τ l : Type := - forall vars, Σ = mapOptionTree ξ vars -> FreshM (ITree _ (fun t => Expr Γ Δ ξ (t@@l)) τ). + forall vars, Σ = mapOptionTree ξ vars -> FreshM (ITree _ (fun t => Expr Γ Δ ξ t l) τ). Definition urule2expr : forall Γ Δ h j t l (r:@Arrange _ h j) (ξ:VV -> LeveledHaskType Γ ★), ujudg2exprType Γ ξ Δ h t l -> @@ -237,49 +238,49 @@ Section HaskProofToStrong. ujudg2exprType Γ ξ Δ H t l -> ujudg2exprType Γ ξ Δ C t l with - | RLeft h c ctx r => let case_RLeft := tt in (fun e => _) (urule2expr _ _ _ _ r) - | RRight h c ctx r => let case_RRight := tt in (fun e => _) (urule2expr _ _ _ _ r) - | RId a => let case_RId := tt in _ - | RCanL a => let case_RCanL := tt in _ - | RCanR a => let case_RCanR := tt in _ - | RuCanL a => let case_RuCanL := tt in _ - | RuCanR a => let case_RuCanR := tt in _ - | RAssoc a b c => let case_RAssoc := tt in _ - | RCossa a b c => let case_RCossa := tt in _ - | RExch a b => let case_RExch := tt in _ - | RWeak a => let case_RWeak := tt in _ - | RCont a => let case_RCont := tt in _ - | RComp a b c f g => let case_RComp := tt in (fun e1 e2 => _) (urule2expr _ _ _ _ f) (urule2expr _ _ _ _ g) + | ALeft h c ctx r => let case_ALeft := tt in (fun e => _) (urule2expr _ _ _ _ r) + | ARight h c ctx r => let case_ARight := tt in (fun e => _) (urule2expr _ _ _ _ r) + | AId a => let case_AId := tt in _ + | ACanL a => let case_ACanL := tt in _ + | ACanR a => let case_ACanR := tt in _ + | AuCanL a => let case_AuCanL := tt in _ + | AuCanR a => let case_AuCanR := tt in _ + | AAssoc a b c => let case_AAssoc := tt in _ + | AuAssoc a b c => let case_AuAssoc := tt in _ + | AExch a b => let case_AExch := tt in _ + | AWeak a => let case_AWeak := tt in _ + | ACont a => let case_ACont := tt in _ + | AComp a b c f g => let case_AComp := tt in (fun e1 e2 => _) (urule2expr _ _ _ _ f) (urule2expr _ _ _ _ g) end); clear urule2expr; intros. - destruct case_RId. + destruct case_AId. apply X. - destruct case_RCanL. + destruct case_ACanL. simpl; unfold ujudg2exprType; intros. simpl in X. apply (X ([],,vars)). simpl; rewrite <- H; auto. - destruct case_RCanR. + destruct case_ACanR. simpl; unfold ujudg2exprType; intros. simpl in X. apply (X (vars,,[])). simpl; rewrite <- H; auto. - destruct case_RuCanL. + destruct case_AuCanL. simpl; unfold ujudg2exprType; intros. destruct vars; try destruct o; inversion H. simpl in X. apply (X vars2); auto. - destruct case_RuCanR. + destruct case_AuCanR. simpl; unfold ujudg2exprType; intros. destruct vars; try destruct o; inversion H. simpl in X. apply (X vars1); auto. - destruct case_RAssoc. + destruct case_AAssoc. simpl; unfold ujudg2exprType; intros. simpl in X. destruct vars; try destruct o; inversion H. @@ -287,7 +288,7 @@ Section HaskProofToStrong. apply (X (vars1_1,,(vars1_2,,vars2))). subst; auto. - destruct case_RCossa. + destruct case_AuAssoc. simpl; unfold ujudg2exprType; intros. simpl in X. destruct vars; try destruct o; inversion H. @@ -295,20 +296,20 @@ Section HaskProofToStrong. apply (X ((vars1,,vars2_1),,vars2_2)). subst; auto. - destruct case_RExch. + destruct case_AExch. simpl; unfold ujudg2exprType ; intros. simpl in X. destruct vars; try destruct o; inversion H. apply (X (vars2,,vars1)). inversion H; subst; auto. - destruct case_RWeak. + destruct case_AWeak. simpl; unfold ujudg2exprType; intros. simpl in X. apply (X []). auto. - destruct case_RCont. + destruct case_ACont. simpl; unfold ujudg2exprType ; intros. simpl in X. apply (X (vars,,vars)). @@ -316,7 +317,7 @@ Section HaskProofToStrong. rewrite <- H. auto. - destruct case_RLeft. + destruct case_ALeft. intro vars; unfold ujudg2exprType; intro H. destruct vars; try destruct o; inversion H. apply (fun q => e ξ q vars2 H2). @@ -331,7 +332,7 @@ Section HaskProofToStrong. simpl. reflexivity. - destruct case_RRight. + destruct case_ARight. intro vars; unfold ujudg2exprType; intro H. destruct vars; try destruct o; inversion H. apply (fun q => e ξ q vars1 H1). @@ -346,7 +347,7 @@ Section HaskProofToStrong. simpl. reflexivity. - destruct case_RComp. + destruct case_AComp. apply e2. apply e1. apply X. @@ -354,7 +355,7 @@ Section HaskProofToStrong. Definition letrec_helper Γ Δ l (varstypes:Tree ??(VV * HaskType Γ ★)) ξ' : ITree (HaskType Γ ★) - (fun t : HaskType Γ ★ => Expr Γ Δ ξ' (t @@ l)) + (fun t : HaskType Γ ★ => Expr Γ Δ ξ' t l) (mapOptionTree (unlev ○ ξ' ○ (@fst _ _)) varstypes) -> ELetRecBindings Γ Δ ξ' l varstypes. intros. @@ -421,7 +422,8 @@ Section HaskProofToStrong. prod (judg2exprType (pcb_judg (projT2 pcb))) {vars' : Tree ??VV & pcb_freevars (projT2 pcb) = mapOptionTree ξ vars'} -> ((fun sac => FreshM { scb : StrongCaseBranchWithVVs VV eqdec_vv tc avars sac - & Expr (sac_gamma sac Γ) (sac_delta sac Γ avars (weakCK'' Δ)) (scbwv_xi scb ξ lev) (weakLT' (tbranches @@ lev)) }) (projT1 pcb)). + & Expr (sac_gamma sac Γ) (sac_delta sac Γ avars (weakCK'' Δ)) (scbwv_xi scb ξ lev) + (weakT' tbranches) (weakL' lev) }) (projT1 pcb)). intro pcb. intro X. simpl in X. @@ -567,8 +569,11 @@ Section HaskProofToStrong. destruct case_RVar. apply ILeaf; simpl; intros; refine (return ILeaf _ _). - destruct vars; simpl in H; inversion H; destruct o. inversion H1. rewrite H2. - apply EVar. + destruct vars; simpl in H; inversion H; destruct o. inversion H1. + set (@EVar _ _ _ Δ ξ v) as q. + rewrite <- H2 in q. + simpl in q. + apply q. inversion H. destruct case_RGlobal. @@ -852,9 +857,9 @@ Section HaskProofToStrong. admit. Defined. - Definition proof2expr Γ Δ τ Σ (ξ0: VV -> LeveledHaskType Γ ★) - {zz:ToString VV} : ND Rule [] [Γ > Δ > Σ |- [unlev τ] @ getlev τ] -> - FreshM (???{ ξ : _ & Expr Γ Δ ξ τ}). + Definition proof2expr Γ Δ τ l Σ (ξ0: VV -> LeveledHaskType Γ ★) + {zz:ToString VV} : ND Rule [] [Γ > Δ > Σ |- [τ] @ l] -> + FreshM (???{ ξ : _ & Expr Γ Δ ξ τ l}). intro pf. set (mkSIND systemfc_all_rules_one_conclusion _ _ _ pf (scnd_weak [])) as cnd. apply closed2expr in cnd. @@ -872,7 +877,6 @@ Section HaskProofToStrong. exists ξ. apply ileaf in it. simpl in it. - destruct τ. apply it. apply INone. Defined.