1 (*********************************************************************************************************************************)
2 (* HaskProofToStrong: convert HaskProof to HaskStrong *)
3 (*********************************************************************************************************************************)
5 Generalizable All Variables.
6 Require Import Preamble.
7 Require Import General.
8 Require Import NaturalDeduction.
9 Require Import Coq.Strings.String.
10 Require Import Coq.Lists.List.
11 Require Import Coq.Init.Specif.
12 Require Import HaskKinds.
13 Require Import HaskStrongTypes.
14 Require Import HaskStrong.
15 Require Import HaskProof.
17 Section HaskProofToStrong.
19 Context {VV:Type} {eqdec_vv:EqDecidable VV} {freshM:FreshMonad VV}.
21 Definition fresh := FMT_fresh freshM.
22 Definition FreshM := FMT freshM.
23 Definition FreshMon := FMT_Monad freshM.
24 Existing Instance FreshMon.
26 Definition ExprVarResolver Γ := VV -> LeveledHaskType Γ ★.
28 Definition ujudg2exprType {Γ}{Δ}(ξ:ExprVarResolver Γ)(j:UJudg Γ Δ) : Type :=
30 mkUJudg Σ τ => forall vars, Σ = mapOptionTree ξ vars ->
31 FreshM (ITree _ (fun t => Expr Γ Δ ξ t) τ)
34 Definition judg2exprType (j:Judg) : Type :=
36 (Γ > Δ > Σ |- τ) => forall (ξ:ExprVarResolver Γ) vars, Σ = mapOptionTree ξ vars ->
37 FreshM (ITree _ (fun t => Expr Γ Δ ξ t) τ)
40 Definition justOne Γ Δ ξ τ : ITree _ (fun t => Expr Γ Δ ξ t) [τ] -> Expr Γ Δ ξ τ.
45 Definition ileaf `(it:ITree X F [t]) : F t.
50 Lemma update_branches : forall Γ (ξ:VV -> LeveledHaskType Γ ★) l1 l2 q,
51 update_ξ ξ (app l1 l2) q = update_ξ (update_ξ ξ l2) l1 q.
61 Lemma mapOptionTree_extensional {A}{B}(f g:A->B) : (forall a, f a = g a) -> (forall t, mapOptionTree f t = mapOptionTree g t).
65 simpl; rewrite H; auto.
66 simpl; rewrite IHt1; rewrite IHt2; auto.
69 Lemma quark {T} (l1:list T) l2 vf :
70 (In vf (app l1 l2)) <->
71 (In vf l1) \/ (In vf l2).
98 right; apply H0; auto.
99 right; apply H0; auto.
102 Lemma splitter {T} (l1:list T) l2 vf :
103 (In vf (app l1 l2) → False)
104 -> (In vf l1 → False) /\ (In vf l2 → False).
106 split; intros; apply H; rewrite quark.
112 : forall T Z {eqdt:EqDecidable T}(tl:Tree ??T)(vf:T) ξ (q:Z),
113 (In vf (leaves tl) -> False) ->
114 mapOptionTree (fun v' => if eqd_dec vf v' then q else ξ v') tl =
120 set (eqd_dec vf t) as x in *.
137 : forall types vars Σ ξ, Σ = mapOptionTree ξ vars ->
138 FreshM { varstypes : _
139 | mapOptionTree (update_ξ(Γ:=Γ) ξ (leaves varstypes)) vars = Σ
140 /\ mapOptionTree (update_ξ ξ (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) = types }.
143 refine (bind vf = fresh (leaves vars) ; return _).
145 destruct vf as [ vf vf_pf ].
149 set (helper VV _ vars vf ξ l vf_pf) as q.
153 destruct (eqd_dec vf vf); [ idtac | set (n (refl_equal _)) as n'; inversion n' ]; auto.
156 intros vars Σ ξ pf; refine (bind x2 = IHtypes2 vars Σ ξ pf; _).
158 destruct x2 as [vt2 [pf21 pf22]].
159 refine (bind x1 = IHtypes1 (vars,,(mapOptionTree (@fst _ _) vt2)) (Σ,,types2) (update_ξ ξ (leaves vt2)) _; return _).
165 clear IHtypes1 IHtypes2.
166 destruct x1 as [vt1 [pf11 pf12]].
167 exists (vt1,,vt2); split; auto.
169 set (update_branches Γ ξ (leaves vt1) (leaves vt2)) as q.
170 set (mapOptionTree_extensional _ _ q) as q'.
177 set (update_branches Γ ξ (leaves vt1) (leaves vt2)) as q.
178 set (mapOptionTree_extensional _ _ q) as q'.
182 rewrite <- mapOptionTree_compose.
183 rewrite <- mapOptionTree_compose.
184 rewrite <- mapOptionTree_compose in *.
187 rewrite <- mapOptionTree_compose.
191 Lemma fresh_lemma Γ ξ vars Σ Σ'
192 : Σ = mapOptionTree ξ vars ->
194 | mapOptionTree (update_ξ(Γ:=Γ) ξ ((vars',Σ')::nil)) vars = Σ
195 /\ mapOptionTree (update_ξ ξ ((vars',Σ')::nil)) [vars'] = [Σ'] }.
197 set (fresh_lemma' Γ [Σ'] vars Σ ξ H) as q.
198 refine (q >>>= fun q' => return _).
201 destruct q' as [varstypes [pf1 pf2]].
202 destruct varstypes; try destruct o; try destruct p; simpl in *.
203 destruct (eqd_dec v v); [ idtac | set (n (refl_equal _)) as n'; inversion n' ].
204 inversion pf2; subst.
206 destruct (eqd_dec v v); [ idtac | set (n (refl_equal _)) as n'; inversion n' ].
212 Lemma manyFresh : forall Γ Σ (ξ0:VV -> LeveledHaskType Γ ★),
213 FreshM { vars : _ & { ξ : VV -> LeveledHaskType Γ ★ & Σ = mapOptionTree ξ vars } }.
215 set (fresh_lemma' Γ Σ [] [] ξ0 (refl_equal _)) as q.
216 refine (q >>>= fun q' => return _).
219 destruct q' as [varstypes [pf1 pf2]].
220 exists (mapOptionTree (@fst _ _) varstypes).
221 exists (update_ξ ξ0 (leaves varstypes)).
225 Definition urule2expr : forall Γ Δ h j (r:@URule Γ Δ h j) (ξ:VV -> LeveledHaskType Γ ★),
226 ITree _ (ujudg2exprType ξ) h -> ITree _ (ujudg2exprType ξ) j.
228 refine (fix urule2expr Γ Δ h j (r:@URule Γ Δ h j) ξ {struct r} :
229 ITree _ (ujudg2exprType ξ) h -> ITree _ (ujudg2exprType ξ) j :=
230 match r as R in URule H C return ITree _ (ujudg2exprType ξ) H -> ITree _ (ujudg2exprType ξ) C with
231 | RLeft h c ctx r => let case_RLeft := tt in (fun e => _) (urule2expr _ _ _ _ r)
232 | RRight h c ctx r => let case_RRight := tt in (fun e => _) (urule2expr _ _ _ _ r)
233 | RCanL t a => let case_RCanL := tt in _
234 | RCanR t a => let case_RCanR := tt in _
235 | RuCanL t a => let case_RuCanL := tt in _
236 | RuCanR t a => let case_RuCanR := tt in _
237 | RAssoc t a b c => let case_RAssoc := tt in _
238 | RCossa t a b c => let case_RCossa := tt in _
239 | RExch t a b => let case_RExch := tt in _
240 | RWeak t a => let case_RWeak := tt in _
241 | RCont t a => let case_RCont := tt in _
242 end); clear urule2expr; intros.
245 apply ILeaf; simpl; intros.
248 apply (X0 ([],,vars)).
249 simpl; rewrite <- H; auto.
252 apply ILeaf; simpl; intros.
255 apply (X0 (vars,,[])).
256 simpl; rewrite <- H; auto.
258 destruct case_RuCanL.
259 apply ILeaf; simpl; intros.
260 destruct vars; try destruct o; inversion H.
263 apply (X0 vars2); auto.
265 destruct case_RuCanR.
266 apply ILeaf; simpl; intros.
267 destruct vars; try destruct o; inversion H.
270 apply (X0 vars1); auto.
272 destruct case_RAssoc.
273 apply ILeaf; simpl; intros.
276 destruct vars; try destruct o; inversion H.
277 destruct vars1; try destruct o; inversion H.
278 apply (X0 (vars1_1,,(vars1_2,,vars2))).
281 destruct case_RCossa.
282 apply ILeaf; simpl; intros.
285 destruct vars; try destruct o; inversion H.
286 destruct vars2; try destruct o; inversion H.
287 apply (X0 ((vars1,,vars2_1),,vars2_2)).
291 destruct c; [ idtac | apply no_urules_with_multiple_conclusions in r0; inversion r0; exists c1; exists c2; auto ].
292 destruct o; [ idtac | apply INone ].
293 destruct u; simpl in *.
294 apply ILeaf; simpl; intros.
295 destruct vars; try destruct o; inversion H.
296 set (fun q => ileaf (e ξ q)) as r'.
298 apply r' with (vars:=vars2).
310 apply X with (vars:=vars1,,vars).
317 apply IHh0_1. inversion X; auto.
318 apply IHh0_2. inversion X; auto.
321 destruct case_RRight.
322 destruct c; [ idtac | apply no_urules_with_multiple_conclusions in r0; inversion r0; exists c1; exists c2; auto ].
323 destruct o; [ idtac | apply INone ].
324 destruct u; simpl in *.
325 apply ILeaf; simpl; intros.
326 destruct vars; try destruct o; inversion H.
327 set (fun q => ileaf (e ξ q)) as r'.
329 apply r' with (vars:=vars1).
341 apply X with (vars:=vars,,vars2).
348 apply IHh0_1. inversion X; auto.
349 apply IHh0_2. inversion X; auto.
353 apply ILeaf; simpl; intros.
356 destruct vars; try destruct o; inversion H.
357 apply (X0 (vars2,,vars1)).
358 inversion H; subst; auto.
361 apply ILeaf; simpl; intros.
368 apply ILeaf; simpl; intros.
371 apply (X0 (vars,,vars)).
377 Definition bridge Γ Δ (c:Tree ??(UJudg Γ Δ)) ξ :
378 ITree Judg judg2exprType (mapOptionTree UJudg2judg c) -> ITree (UJudg Γ Δ) (ujudg2exprType ξ) c.
382 destruct u; simpl in *.
386 intros; apply it with (vars:=vars); auto.
388 apply IBranch; [ apply IHc1 | apply IHc2 ]; inversion it; auto.
391 Definition letrec_helper Γ Δ l varstypes ξ' :
392 ITree (LeveledHaskType Γ ★)
393 (fun t : LeveledHaskType Γ ★ => Expr Γ Δ ξ' t)
394 (mapOptionTree (ξ' ○ (@fst _ _)) varstypes)
395 -> ELetRecBindings Γ Δ ξ' l
396 (mapOptionTree (fun x : VV * LeveledHaskType Γ ★ => ⟨fst x, unlev (snd x) ⟩) varstypes).
399 destruct a; simpl in *.
401 destruct l0 as [τ l'].
403 apply ileaf in X. simpl in X.
404 destruct (eqd_dec (unlev (ξ' v)) τ).
409 destruct (eqd_dec h0 l).
412 apply (Prelude_error "level mismatch; should never happen").
413 apply (Prelude_error "letrec type mismatch; should never happen").
417 simpl; apply ELR_branch.
427 Lemma leaves_unleaves {T}(t:list T) : leaves (unleaves t) = t.
433 Definition case_helper tc Γ Δ lev tbranches avars ξ (Σ:Tree ??VV) :
434 forall pcb : ProofCaseBranch tc Γ Δ lev tbranches avars,
435 judg2exprType (pcb_judg pcb) ->
436 (pcb_freevars pcb) = mapOptionTree ξ Σ ->
438 {scb : StrongCaseBranchWithVVs VV eqdec_vv tc avars &
439 Expr (sac_Γ scb Γ) (sac_Δ scb Γ avars (weakCK'' Δ))
440 (scbwv_ξ scb ξ lev) (weakLT' (tbranches @@ lev))}.
445 set (sac_types pcb_scb _ avars) as boundvars.
446 refine (fresh_lemma' _ (unleaves (map (fun x => x@@(weakL' lev)) (vec2list boundvars))) Σ
447 (mapOptionTree weakLT' pcb_freevars)
449 >>>= fun ξvars => _). apply FreshMon.
451 rewrite <- mapOptionTree_compose.
453 destruct ξvars as [ exprvars [pf1 pf2 ]].
454 set (list2vec (leaves (mapOptionTree (@fst _ _) exprvars))) as exprvars'.
455 assert (sac_numExprVars pcb_scb = Datatypes.length (leaves (mapOptionTree (@fst _ _) exprvars))) as H'.
456 rewrite <- mapOptionTree_compose in pf2.
459 rewrite <- map_preserves_length.
460 rewrite map_preserves_length with (f:=update_ξ (weakLT' ○ ξ) (leaves exprvars) ○ (@fst _ _)).
461 rewrite <- mapleaves.
463 rewrite leaves_unleaves.
464 rewrite vec2list_map_list2vec.
465 rewrite vec2list_len.
467 rewrite <- H' in exprvars'.
470 set (@Build_StrongCaseBranchWithVVs VV _ tc _ avars pcb_scb exprvars') as scb.
471 set (scbwv_ξ scb ξ lev) as ξ'.
472 refine (X ξ' (Σ,,(unleaves (vec2list exprvars'))) _ >>>= fun X' => return _). apply FreshMon.
477 rewrite <- vec2list_map_list2vec.
489 Fixpoint treeM {T}(t:Tree ??(FreshM T)) : FreshM (Tree ??T) :=
491 | T_Leaf None => return []
492 | T_Leaf (Some x) => bind x' = x ; return [x']
493 | T_Branch b1 b2 => bind b1' = treeM b1 ; bind b2' = treeM b2 ; return (b1',,b2')
496 Lemma itree_mapOptionTree : forall T T' F (f:T->T') t,
497 ITree _ F (mapOptionTree f t) ->
500 induction t; try destruct a; simpl in *.
505 apply IHt1; inversion X; auto.
506 apply IHt2; inversion X; auto.
509 Definition rule2expr : forall h j (r:Rule h j), ITree _ judg2exprType h -> ITree _ judg2exprType j.
513 refine (match r as R in Rule H C return ITree _ judg2exprType H -> ITree _ judg2exprType C with
514 | RURule a b c d e => let case_RURule := tt in _
515 | RNote Γ Δ Σ τ l n => let case_RNote := tt in _
516 | RLit Γ Δ l _ => let case_RLit := tt in _
517 | RVar Γ Δ σ p => let case_RVar := tt in _
518 | RGlobal Γ Δ σ l wev => let case_RGlobal := tt in _
519 | RLam Γ Δ Σ tx te x => let case_RLam := tt in _
520 | RCast Γ Δ Σ σ τ γ x => let case_RCast := tt in _
521 | RAbsT Γ Δ Σ κ σ a => let case_RAbsT := tt in _
522 | RAppT Γ Δ Σ κ σ τ y => let case_RAppT := tt in _
523 | RAppCo Γ Δ Σ κ σ₁ σ₂ γ σ l => let case_RAppCo := tt in _
524 | RAbsCo Γ Δ Σ κ σ σ₁ σ₂ y => let case_RAbsCo := tt in _
525 | RApp Γ Δ Σ₁ Σ₂ tx te p => let case_RApp := tt in _
526 | RLet Γ Δ Σ₁ Σ₂ σ₁ σ₂ p => let case_RLet := tt in _
527 | RBindingGroup Γ p lri m x q => let case_RBindingGroup := tt in _
528 | REmptyGroup _ _ => let case_REmptyGroup := tt in _
529 | RBrak Σ a b c n m => let case_RBrak := tt in _
530 | REsc Σ a b c n m => let case_REsc := tt in _
531 | RCase Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt in _
532 | RLetRec Γ Δ lri x y => let case_RLetRec := tt in _
533 end); intro X_; try apply ileaf in X_; simpl in X_.
535 destruct case_RURule.
536 destruct d; try destruct o.
537 apply ILeaf; destruct u; simpl; intros.
538 set (@urule2expr a b _ _ e ξ) as q.
539 set (fun z => ileaf (q z)) as q'.
541 apply q' with (vars:=vars).
546 apply no_urules_with_empty_conclusion in e; inversion e; auto.
547 apply no_urules_with_multiple_conclusions in e; inversion e; auto; exists d1; exists d2; auto.
550 apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
555 apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
560 apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
565 apply ILeaf; simpl; intros; refine (return ILeaf _ _).
569 apply ILeaf; simpl; intros; refine (return ILeaf _ _).
570 destruct vars; simpl in H; inversion H; destruct o. inversion H1. rewrite H2.
574 destruct case_RGlobal.
575 apply ILeaf; simpl; intros; refine (return ILeaf _ _).
582 refine (fresh_lemma _ ξ vars _ (tx@@x) H >>>= (fun pf => _)).
584 destruct pf as [ vnew [ pf1 pf2 ]].
585 set (update_ξ ξ ((⟨vnew, tx @@ x ⟩) :: nil)) as ξ' in *.
586 refine (X_ ξ' (vars,,[vnew]) _ >>>= _).
596 apply ELam with (ev:=vnew).
603 apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
606 apply ileaf in X. simpl in X.
609 destruct case_RBindingGroup.
610 apply ILeaf; simpl; intros.
615 destruct vars; inversion H.
616 destruct o; inversion H3.
617 refine (X ξ vars1 H3 >>>= fun X' => X0 ξ vars2 H4 >>>= fun X0' => return _).
629 destruct vars. try destruct o; inversion H.
632 set (X1 ξ vars1 H5) as q1.
633 set (X2 ξ vars2 H6) as q2.
634 refine (q1 >>>= fun q1' => q2 >>>= fun q2' => return _).
641 apply (EApp _ _ _ _ _ _ q1' q2').
646 destruct vars; try destruct o; inversion H.
647 refine (fresh_lemma _ ξ vars1 _ (σ₂@@p) H1 >>>= (fun pf => _)).
649 destruct pf as [ vnew [ pf1 pf2 ]].
650 set (update_ξ ξ ((⟨vnew, σ₂ @@ p ⟩) :: nil)) as ξ' in *.
655 refine (X0 ξ vars2 _ >>>= fun X0' => _).
658 refine (X ξ' (vars1,,[vnew]) _ >>>= fun X1' => _).
671 apply ELet with (ev:=vnew)(tv:=σ₂).
675 destruct case_REmptyGroup.
676 apply ILeaf; simpl; intros.
681 apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
686 apply ILeaf; simpl; intros; refine (X_ (weakLT ○ ξ) vars _ >>>= fun X => return ILeaf _ _). apply FreshMon.
687 rewrite mapOptionTree_compose.
690 apply ileaf in X. simpl in *.
694 destruct case_RAppCo.
695 apply ILeaf; simpl; intros; refine (X_ ξ vars _ >>>= fun X => return ILeaf _ _). apply FreshMon.
701 destruct case_RAbsCo.
702 apply ILeaf; simpl; intros; refine (X_ ξ vars _ >>>= fun X => return ILeaf _ _). apply FreshMon.
707 destruct case_RLetRec.
708 apply ILeaf; simpl; intros.
709 refine (bind ξvars = fresh_lemma' _ y _ _ _ H; _). apply FreshMon.
710 destruct ξvars as [ varstypes [ pf1 pf2 ]].
711 refine (X_ ((update_ξ ξ (leaves varstypes)))
712 (vars,,(mapOptionTree (@fst _ _) varstypes)) _ >>>= fun X => return _); clear X_. apply FreshMon.
719 inversion X; subst; clear X.
721 (* getting rid of this will require strengthening RLetRec *)
722 assert ((mapOptionTree (fun x : VV * LeveledHaskType Γ ★ => ⟨fst x, unlev (snd x) @@ l ⟩) varstypes) = varstypes) as HHH.
725 apply (@ELetRec _ _ _ _ _ _ _ (mapOptionTree (fun x => ((fst x),unlev (snd x))) varstypes));
726 rewrite mapleaves; rewrite <- map_compose; simpl;
728 | rewrite <- mapleaves; rewrite HHH; apply (ileaf X0) ].
731 rewrite <- mapOptionTree_compose in X1.
732 set (fun x : VV * LeveledHaskType Γ ★ => ⟨fst x, unlev (snd x) @@ l ⟩) as ξ' in *.
733 rewrite <- mapleaves.
736 apply (letrec_helper _ _ _ _ _ X1).
739 apply ILeaf; simpl; intros.
745 set (mapOptionTreeAndFlatten pcb_freevars alts) as Σalts in *.
746 refine (bind ξvars = fresh_lemma' _ (Σalts,,Σ) _ _ _ H ; _).
748 destruct vars; try destruct o; inversion H; clear H.
749 rename vars1 into varsalts.
750 rename vars2 into varsΣ.
753 refine ( _ >>>= fun Y => X0 ξ varsΣ _ >>>= fun X => return ILeaf _ (@ECase _ _ _ _ _ _ _ _ _ (ileaf X) Y)); auto.
755 destruct ξvars as [varstypes [pf1 pf2]].
758 apply itree_mapOptionTree in X.
759 refine (itree_to_tree (itmap _ X)).
763 instantiate (1:=varsΣ).
769 Definition closed2expr : forall c (pn:@ClosedND _ Rule c), ITree _ judg2exprType c.
771 fix closed2expr' j (pn:@ClosedND _ Rule j) {struct pn} : ITree _ judg2exprType j :=
772 match pn in @ClosedND _ _ J return ITree _ judg2exprType J with
773 | cnd_weak => let case_nil := tt in INone _ _
774 | cnd_rule h c cnd' r => let case_rule := tt in rule2expr _ _ r (closed2expr' _ cnd')
775 | cnd_branch _ _ c1 c2 => let case_branch := tt in IBranch _ _ (closed2expr' _ c1) (closed2expr' _ c2)
776 end)); clear closed2expr'; intros; subst.
779 Definition proof2expr Γ Δ τ Σ (ξ0: VV -> LeveledHaskType Γ ★)
780 {zz:ToString VV} : ND Rule [] [Γ > Δ > Σ |- [τ]] ->
781 FreshM (???{ ξ : _ & Expr Γ Δ ξ τ}).
783 set (closedFromSCND _ _ (mkSCND systemfc_all_rules_one_conclusion _ _ _ pf (scnd_weak [])) cnd_weak) as cnd.
784 apply closed2expr in cnd.
788 refine (bind ξvars = manyFresh _ Σ ξ0; _).
790 destruct ξvars as [vars ξpf].
791 destruct ξpf as [ξ pf].
792 refine (cnd ξ vars _ >>>= fun it => _).
795 refine (return OK _).
800 End HaskProofToStrong.