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 assert (unlev (ξ' v) = τ).
412 assert (h0=l). admit.
418 simpl; apply ELR_branch.
430 Definition case_helper tc Γ Δ lev tbranches avars ξ (Σ:Tree ??VV) tys :
431 forall pcb : ProofCaseBranch tc Γ Δ lev tbranches avars,
432 judg2exprType (pcb_judg pcb) -> FreshM
433 {scb : StrongCaseBranchWithVVs VV eqdec_vv tc avars &
434 Expr (sac_Γ scb Γ) (sac_Δ scb Γ avars (weakCK'' Δ))
435 (scbwv_ξ scb ξ lev) (weakLT' (tbranches @@ lev))}.
440 refine (bind ξvars = fresh_lemma' Γ pcb_freevars Σ [] ξ _ ; _). apply FreshMon.
441 destruct ξvars as [vars [ξ'
445 Lemma itree_mapOptionTree : forall T T' F (f:T->T') t,
446 ITree _ F (mapOptionTree f t) ->
449 induction t; try destruct a; simpl in *.
454 apply IHt1; inversion X; auto.
455 apply IHt2; inversion X; auto.
458 Definition rule2expr : forall h j (r:Rule h j), ITree _ judg2exprType h -> ITree _ judg2exprType j.
462 refine (match r as R in Rule H C return ITree _ judg2exprType H -> ITree _ judg2exprType C with
463 | RURule a b c d e => let case_RURule := tt in _
464 | RNote Γ Δ Σ τ l n => let case_RNote := tt in _
465 | RLit Γ Δ l _ => let case_RLit := tt in _
466 | RVar Γ Δ σ p => let case_RVar := tt in _
467 | RGlobal Γ Δ σ l wev => let case_RGlobal := tt in _
468 | RLam Γ Δ Σ tx te x => let case_RLam := tt in _
469 | RCast Γ Δ Σ σ τ γ x => let case_RCast := tt in _
470 | RAbsT Γ Δ Σ κ σ a => let case_RAbsT := tt in _
471 | RAppT Γ Δ Σ κ σ τ y => let case_RAppT := tt in _
472 | RAppCo Γ Δ Σ κ σ₁ σ₂ γ σ l => let case_RAppCo := tt in _
473 | RAbsCo Γ Δ Σ κ σ σ₁ σ₂ y => let case_RAbsCo := tt in _
474 | RApp Γ Δ Σ₁ Σ₂ tx te p => let case_RApp := tt in _
475 | RLet Γ Δ Σ₁ Σ₂ σ₁ σ₂ p => let case_RLet := tt in _
476 | RBindingGroup Γ p lri m x q => let case_RBindingGroup := tt in _
477 | REmptyGroup _ _ => let case_REmptyGroup := tt in _
478 | RBrak Σ a b c n m => let case_RBrak := tt in _
479 | REsc Σ a b c n m => let case_REsc := tt in _
480 | RCase Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt in _
481 | RLetRec Γ Δ lri x y => let case_RLetRec := tt in _
482 end); intro X_; try apply ileaf in X_; simpl in X_.
484 destruct case_RURule.
485 destruct d; try destruct o.
486 apply ILeaf; destruct u; simpl; intros.
487 set (@urule2expr a b _ _ e ξ) as q.
488 set (fun z => ileaf (q z)) as q'.
490 apply q' with (vars:=vars).
495 apply no_urules_with_empty_conclusion in e; inversion e; auto.
496 apply no_urules_with_multiple_conclusions in e; inversion e; auto; exists d1; exists d2; auto.
499 apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
504 apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
509 apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
514 apply ILeaf; simpl; intros; refine (return ILeaf _ _).
518 apply ILeaf; simpl; intros; refine (return ILeaf _ _).
519 destruct vars; simpl in H; inversion H; destruct o. inversion H1. rewrite H2.
523 destruct case_RGlobal.
524 apply ILeaf; simpl; intros; refine (return ILeaf _ _).
531 refine (fresh_lemma _ ξ vars _ (tx@@x) H >>>= (fun pf => _)).
533 destruct pf as [ vnew [ pf1 pf2 ]].
534 set (update_ξ ξ ((⟨vnew, tx @@ x ⟩) :: nil)) as ξ' in *.
535 refine (X_ ξ' (vars,,[vnew]) _ >>>= _).
545 apply ELam with (ev:=vnew).
552 apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
555 apply ileaf in X. simpl in X.
558 destruct case_RBindingGroup.
559 apply ILeaf; simpl; intros.
564 destruct vars; inversion H.
565 destruct o; inversion H3.
566 refine (X ξ vars1 H3 >>>= fun X' => X0 ξ vars2 H4 >>>= fun X0' => return _).
578 destruct vars. try destruct o; inversion H.
581 set (X1 ξ vars1 H5) as q1.
582 set (X2 ξ vars2 H6) as q2.
583 refine (q1 >>>= fun q1' => q2 >>>= fun q2' => return _).
590 apply (EApp _ _ _ _ _ _ q1' q2').
595 destruct vars; try destruct o; inversion H.
596 refine (fresh_lemma _ ξ vars1 _ (σ₂@@p) H1 >>>= (fun pf => _)).
598 destruct pf as [ vnew [ pf1 pf2 ]].
599 set (update_ξ ξ ((⟨vnew, σ₂ @@ p ⟩) :: nil)) as ξ' in *.
604 refine (X0 ξ vars2 _ >>>= fun X0' => _).
607 refine (X ξ' (vars1,,[vnew]) _ >>>= fun X1' => _).
620 apply ELet with (ev:=vnew)(tv:=σ₂).
624 destruct case_REmptyGroup.
625 apply ILeaf; simpl; intros.
630 apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
635 apply ILeaf; simpl; intros; refine (X_ (weakLT ○ ξ) vars _ >>>= fun X => return ILeaf _ _). apply FreshMon.
636 rewrite mapOptionTree_compose.
639 apply ileaf in X. simpl in *.
643 destruct case_RAppCo.
644 apply ILeaf; simpl; intros; refine (X_ ξ vars _ >>>= fun X => return ILeaf _ _). apply FreshMon.
650 destruct case_RAbsCo.
651 apply ILeaf; simpl; intros; refine (X_ ξ vars _ >>>= fun X => return ILeaf _ _). apply FreshMon.
656 destruct case_RLetRec.
657 apply ILeaf; simpl; intros.
658 refine (bind ξvars = fresh_lemma' _ y _ _ _ H; _). apply FreshMon.
659 destruct ξvars as [ varstypes [ pf1 pf2 ]].
660 refine (X_ ((update_ξ ξ (leaves varstypes)))
661 (vars,,(mapOptionTree (@fst _ _) varstypes)) _ >>>= fun X => return _); clear X_. apply FreshMon.
668 inversion X; subst; clear X.
670 (* getting rid of this will require strengthening RLetRec *)
671 assert ((mapOptionTree (fun x : VV * LeveledHaskType Γ ★ => ⟨fst x, unlev (snd x) @@ l ⟩) varstypes) = varstypes) as HHH.
674 apply (@ELetRec _ _ _ _ _ _ _ (mapOptionTree (fun x => ((fst x),unlev (snd x))) varstypes));
675 rewrite mapleaves; rewrite <- map_compose; simpl;
677 | rewrite <- mapleaves; rewrite HHH; apply (ileaf X0) ].
680 rewrite <- mapOptionTree_compose in X1.
681 set (fun x : VV * LeveledHaskType Γ ★ => ⟨fst x, unlev (snd x) @@ l ⟩) as ξ' in *.
682 rewrite <- mapleaves.
685 apply (letrec_helper _ _ _ _ _ X1).
691 apply (Prelude_error "FIXME").
695 apply ILeaf; simpl; intros.
701 set (mapOptionTreeAndFlatten pcb_freevars alts) as Σalts in *.
702 refine (bind ξvars = fresh_lemma' _ (Σalts,,Σ) _ _ _ H ; _).
704 destruct vars; try destruct o; inversion H; clear H.
705 rename vars1 into varsalts.
706 rename vars2 into varsΣ.
708 refine (X0 ξ varsΣ _ >>>= fun X => return ILeaf _ _); auto. apply FreshMon.
710 eapply (ECase _ _ _ _ _ _ _ (ileaf X1)).
713 destruct ξvars as [varstypes [pf1 pf2]].
715 apply itree_mapOptionTree in X.
716 refine (itree_to_tree (itmap _ X)).
721 Definition closed2expr : forall c (pn:@ClosedND _ Rule c), ITree _ judg2exprType c.
723 fix closed2expr' j (pn:@ClosedND _ Rule j) {struct pn} : ITree _ judg2exprType j :=
724 match pn in @ClosedND _ _ J return ITree _ judg2exprType J with
725 | cnd_weak => let case_nil := tt in INone _ _
726 | cnd_rule h c cnd' r => let case_rule := tt in rule2expr _ _ r (closed2expr' _ cnd')
727 | cnd_branch _ _ c1 c2 => let case_branch := tt in IBranch _ _ (closed2expr' _ c1) (closed2expr' _ c2)
728 end)); clear closed2expr'; intros; subst.
731 Definition proof2expr Γ Δ τ Σ (ξ0: VV -> LeveledHaskType Γ ★)
732 {zz:ToString VV} : ND Rule [] [Γ > Δ > Σ |- [τ]] ->
733 FreshM (???{ ξ : _ & Expr Γ Δ ξ τ}).
735 set (closedFromSCND _ _ (mkSCND systemfc_all_rules_one_conclusion _ _ _ pf (scnd_weak [])) cnd_weak) as cnd.
736 apply closed2expr in cnd.
740 refine (bind ξvars = manyFresh _ Σ ξ0; _).
742 destruct ξvars as [vars ξpf].
743 destruct ξpf as [ξ pf].
744 refine (cnd ξ vars _ >>>= fun it => _).
747 refine (return OK _).
752 End HaskProofToStrong.