| EBrak Γ Δ ξ ec t lev e => expr2antecedent e
| ECast Γ Δ ξ γ t1 t2 lev e => expr2antecedent e
| ENote Γ Δ ξ t l n e => expr2antecedent e
- | ETyLam Γ Δ ξ κ σ l e => expr2antecedent e
+ | ETyLam Γ Δ ξ κ σ l n e => expr2antecedent e
| ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e => expr2antecedent e
| ECoApp Γ Δ κ γ σ₁ σ₂ σ ξ l e => expr2antecedent e
| ETyApp Γ Δ κ σ τ ξ l e => expr2antecedent e
| ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecContext b1),,(eLetRecContext b2)
end.
-Definition mkProofCaseBranch {Γ}{Δ}{ξ}{l}{tc}{tbranches}{atypes}
-(alt : { sac : _ & { scb : StrongCaseBranchWithVVs _ _ tc atypes sac
- & Expr (sac_gamma sac Γ)
- (sac_delta sac Γ atypes (weakCK'' Δ))
- (scbwv_xi scb ξ l)
- (weakT' tbranches) (weakL' l) } })
- : { sac : _ & ProofCaseBranch tc Γ Δ l tbranches atypes sac }.
- destruct alt.
- exists x.
- exact
- {| pcb_freevars := mapOptionTree ξ
- (stripOutVars (vec2list (scbwv_exprvars (projT1 s)))
- (expr2antecedent (projT2 s)))
- |}.
- Defined.
-
-
Fixpoint eLetRecTypes {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??(HaskType Γ ★) :=
match elrb with
| ELR_nil Γ Δ ξ lev => []
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))),
eapply nd_comp; [ idtac | eapply nd_rule; apply z ].
clear z.
- set (@factorContextRightAndWeaken'' Γ Δ pctx ξ' (eLetRecContext branches,,expr2antecedent body)) as q'.
+ set (@factorContextLeftAndWeaken'' Γ Δ pctx ξ' (eLetRecContext branches,,expr2antecedent body)) as q'.
unfold passback in *; clear passback.
unfold pctx in *; clear pctx.
set (q' disti) as q''.
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,
Qed.
+Definition mkProofCaseBranch {Γ}{Δ}{ξ}{l}{tc}{tbranches}{atypes}
+(alt : { sac : _ & { scb : StrongCaseBranchWithVVs _ _ tc atypes sac
+ & Expr (sac_gamma sac Γ)
+ (sac_delta sac Γ atypes (weakCK'' Δ))
+ (scbwv_xi scb ξ l)
+ (weakT' tbranches) (weakL' l) } })
+ : @StrongAltCon tc * Tree ??(LeveledHaskType Γ ★).
+ destruct alt.
+ split.
+ apply x.
+ apply (mapOptionTree ξ
+ (stripOutVars (vec2list (scbwv_exprvars (projT1 s)))
+ (expr2antecedent (projT2 s)))).
+ Defined.
+
Lemma case_lemma : forall Γ Δ ξ l tc tbranches atypes e
(alts':Tree
??{sac : StrongAltCon &
Expr (sac_gamma sac Γ) (sac_delta sac Γ atypes (weakCK'' Δ))
(scbwv_xi scb ξ l) (weakT' tbranches) (weakL' l)}}),
- (mapOptionTreeAndFlatten (fun x => pcb_freevars (projT2 x))
+ (mapOptionTreeAndFlatten (fun x => snd x)
(mapOptionTree mkProofCaseBranch alts'))
,,
mapOptionTree ξ (expr2antecedent e) =
| EBrak Γ Δ ξ ec t lev e => let case_EBrak := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
| ECast Γ Δ ξ γ t1 t2 lev e => let case_ECast := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
| ENote Γ Δ ξ t _ n e => let case_ENote := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
- | ETyLam Γ Δ ξ κ σ l e => let case_ETyLam := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
+ | ETyLam Γ Δ ξ κ σ l n e => let case_ETyLam := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
| ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e => let case_ECoLam := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
| ECoApp Γ Δ κ σ₁ σ₂ σ γ ξ l e => let case_ECoApp := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
| ETyApp Γ Δ κ σ τ ξ l e => let case_ETyApp := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
(sac_delta sac Γ atypes (weakCK'' Δ))
(scbwv_xi scb ξ l)
(weakT' tbranches) (weakL' l) } })
- : ND Rule [] (mapOptionTree (fun x => pcb_judg (projT2 (mkProofCaseBranch x))) alts) :=
+ : ND Rule [] (mapOptionTree (fun x => pcb_judg (snd (mkProofCaseBranch x))) alts) :=
match alts as ALTS return ND Rule []
- (mapOptionTree (fun x => pcb_judg (projT2 (mkProofCaseBranch x))) ALTS) with
+ (mapOptionTree (fun x => pcb_judg (snd (mkProofCaseBranch x))) ALTS) with
| T_Leaf None => let case_nil := tt in _
| T_Branch b1 b2 => let case_branch := tt in (fun b1' b2' => _) (mkdcsp b1) (mkdcsp b2)
| T_Leaf (Some x) =>
- match x as X return ND Rule [] [pcb_judg (projT2 (mkProofCaseBranch X))] with
+ match x as X return ND Rule [] [@pcb_judg tc Γ Δ l tbranches atypes
+ (fst (mkProofCaseBranch X))
+ (snd (mkProofCaseBranch X))] with
existT sac (existT scbx ex) =>
(fun e' => let case_leaf := tt in _) (expr2proof _ _ _ _ _ ex)
end
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.
destruct case_leaf.
clear o x alts alts' e.
- eapply nd_comp; [ apply e' | idtac ].
+ simpl.
+ apply (fun x => nd_comp e' x).
clear e'.
- apply nd_rule.
- apply RArrange.
+ unfold pcb_judg.
simpl.
rewrite mapleaves'.
simpl.
rewrite <- mapleaves'.
rewrite vec2list_map_list2vec.
unfold sac_gamma.
- rewrite <- (scbwv_coherent scbx l ξ).
rewrite <- vec2list_map_list2vec.
rewrite mapleaves'.
- set (@factorContextRightAndWeaken'') as q.
- unfold scbwv_xi.
set (@updating_stripped_tree_is_inert' _ (weakL' l) (weakLT' ○ ξ) (vec2list (scbwv_varstypes scbx))) as z.
unfold scbwv_varstypes in z.
rewrite vec2list_map_list2vec in z.
rewrite fst_zip in z.
rewrite <- z.
clear z.
+ unfold sac_gamma in *.
+ simpl in *.
+ Unset Printing Implicit.
+ idtac.
+ apply nd_rule.
+ apply RArrange.
+ set (scbwv_exprvars_distinct scbx) as q'.
+ rewrite <- leaves_unleaves in q'.
+ apply (AComp (@factorContextRightAndWeaken'' _ (weakCE' Δ) _ _ (expr2antecedent ex) q')).
+ clear q'.
- replace (stripOutVars (vec2list (scbwv_exprvars scbx))) with
- (stripOutVars (leaves (unleaves (vec2list (scbwv_exprvars scbx))))).
- apply q.
- apply (sac_delta sac Γ atypes (weakCK'' Δ)).
- rewrite leaves_unleaves.
- apply (scbwv_exprvars_distinct scbx).
+ set (scbwv_coherent scbx l ξ) as H.
rewrite leaves_unleaves.
- reflexivity.
+ unfold scbwv_varstypes.
+ apply ALeft.
+ rewrite <- mapleaves'.
+ rewrite <- mapleaves'.
+ rewrite mapleaves'.
+ rewrite vec2list_map_list2vec.
+ rewrite <- H.
+ clear H.
+ rewrite <- mapleaves'.
+ rewrite vec2list_map_list2vec.
+ unfold scbwv_xi.
+ unfold scbwv_varstypes.
+ apply AId.
destruct case_nil.
apply nd_id0.
projects / coq-hetmet.git / blobdiff