X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskSkolemizer.v;h=435b687968922e3066467e7a89b2ddba38b51785;hp=c1b570851ac5fb102f0264fbb0256a7fa3d8429b;hb=af41ffb1692ae207554342ccdc3bf73abaa75a01;hpb=4a32fb619ddda1fedb0855a0c7acad0a41704da8 diff --git a/src/HaskSkolemizer.v b/src/HaskSkolemizer.v index c1b5708..435b687 100644 --- a/src/HaskSkolemizer.v +++ b/src/HaskSkolemizer.v @@ -9,6 +9,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. @@ -66,57 +67,50 @@ Section HaskSkolemizer. | a::b => mkArrows b (a ---> t) end. +(* Fixpoint unleaves_ {Γ}(t:Tree ??(LeveledHaskType Γ ★))(l:list (HaskType Γ ★)) lev : Tree ??(LeveledHaskType Γ ★) := match l with | nil => t | a::b => unleaves_ (t,,[a @@ lev]) b lev end. - - (* rules of skolemized proofs *) - Definition getΓ (j:Judg) := match j with Γ > _ > _ |- _ => Γ end. - Definition getSuc (j:Judg) : Tree ??(LeveledHaskType (getΓ j) ★) := - match j as J return Tree ??(LeveledHaskType (getΓ J) ★) with Γ > _ > _ |- s => s end. - Fixpoint getjlev {Γ}(tt:Tree ??(LeveledHaskType Γ ★)) : HaskLevel Γ := - match tt with - | T_Leaf None => nil - | T_Leaf (Some (_ @@ lev)) => lev - | T_Branch b1 b2 => - match getjlev b1 with - | nil => getjlev b2 - | lev => lev - end +*) + (* weak inverse of "leaves" *) + Fixpoint unleaves_ {A:Type}(l:list A) : Tree (option A) := + match l with + | nil => [] + | (a::nil) => [a] + | (a::b) => [a],,(unleaves_ b) end. - Definition ite_unit : ∀ Γ, InstantiatedTypeEnv (fun _ => unit) Γ. - intros. - induction Γ. - apply INil. - apply ICons; auto. - apply tt. - Defined. + (* rules of skolemized proofs *) + Definition getΓ (j:Judg) := match j with Γ > _ > _ |- _ @ _ => Γ end. - Fixpoint grab (n:nat) {T} (l:list T) : T := - match l with - | nil => Prelude_error "grab failed" - | h::t => match n with - | 0 => h - | S n' => grab n' t - end - end. + Fixpoint take_trustme {Γ} + (n:nat) + (l:forall TV, InstantiatedTypeEnv TV Γ -> list (RawHaskType TV ★)) + : list (HaskType Γ ★) := - Fixpoint count' (n:nat)(ln:list nat) : list nat := match n with - | 0 => ln - | S n' => count' n' (n'::ln) + | 0 => nil + | S n' => (fun TV ite => match l TV ite with + | nil => Prelude_error "impossible" + | a::b => a + end) + :: + take_trustme n' (fun TV ite => match l TV ite with + | nil => Prelude_error "impossible" + | a::b => b + end) end. + + Axiom phoas_extensionality : forall Γ Q (f g:forall TV, InstantiatedTypeEnv TV Γ -> Q TV), + (forall tv ite, f tv ite = g tv ite) -> f=g. - Definition count (n:nat) := count' n nil. - - Definition rebundle {Γ}(X:forall TV, InstantiatedTypeEnv TV Γ -> list (RawHaskType TV ★)) : list (HaskType Γ ★ ) := - map (fun n => fun TV ite => grab n (X TV ite)) (count (length (X _ (ite_unit _)))). - - Definition take_arg_types_as_tree Γ (ht:HaskType Γ ★) := - (unleaves' (rebundle (fun TV ite => (take_arg_types (ht TV ite))))). + Definition take_arg_types_as_tree {Γ}(ht:HaskType Γ ★) : Tree ??(HaskType Γ ★ ) := + unleaves_ + (take_trustme + (count_arg_types (ht _ (ite_unit _))) + (fun TV ite => take_arg_types (ht TV ite))). Definition drop_arg_types_as_tree {Γ} (ht:HaskType Γ ★) : HaskType Γ ★ := fun TV ite => drop_arg_types (ht TV ite). @@ -124,13 +118,47 @@ Section HaskSkolemizer. Implicit Arguments take_arg_types_as_tree [[Γ]]. Implicit Arguments drop_arg_types_as_tree [[Γ]]. - Lemma take_works : forall {Γ}(t1 t2:HaskType Γ ★), - take_arg_types_as_tree (t1 ---> t2) = [t1],,(take_arg_types_as_tree t2). + Definition take_arrange : forall {Γ} (tx te:HaskType Γ ★) lev, + Arrange ([tx @@ lev],,take_arg_types_as_tree te @@@ lev) + (take_arg_types_as_tree (tx ---> te) @@@ lev). intros. - unfold take_arg_types_as_tree; simpl. - unfold rebundle at 1. - admit. - Qed. + destruct (eqd_dec ([tx],,take_arg_types_as_tree te) (take_arg_types_as_tree (tx ---> te))). + rewrite <- e. + simpl. + apply AId. + unfold take_arg_types_as_tree. + Opaque take_arg_types_as_tree. + simpl. + destruct (count_arg_types (te (fun _ : Kind => unit) (ite_unit Γ))). + simpl. + replace (tx) with (fun (TV : Kind → Type) (ite : InstantiatedTypeEnv TV Γ) => tx TV ite). + apply ACanR. + apply phoas_extensionality. + reflexivity. + apply (Prelude_error "should not be possible"). + Defined. + Transparent take_arg_types_as_tree. + + Definition take_unarrange : forall {Γ} (tx te:HaskType Γ ★) lev, + Arrange (take_arg_types_as_tree (tx ---> te) @@@ lev) + ([tx @@ lev],,take_arg_types_as_tree te @@@ lev). + intros. + destruct (eqd_dec ([tx],,take_arg_types_as_tree te) (take_arg_types_as_tree (tx ---> te))). + rewrite <- e. + simpl. + apply AId. + unfold take_arg_types_as_tree. + Opaque take_arg_types_as_tree. + simpl. + destruct (count_arg_types (te (fun _ : Kind => unit) (ite_unit Γ))). + simpl. + replace (tx) with (fun (TV : Kind → Type) (ite : InstantiatedTypeEnv TV Γ) => tx TV ite). + apply AuCanR. + apply phoas_extensionality. + reflexivity. + apply (Prelude_error "should not be possible"). + Defined. + Transparent take_arg_types_as_tree. Lemma drop_works : forall {Γ}(t1 t2:HaskType Γ ★), drop_arg_types_as_tree (t1 ---> t2) = (drop_arg_types_as_tree t2). @@ -145,13 +173,13 @@ Section HaskSkolemizer. | SFlat : forall h c, Rule h c -> SRule h c | SBrak : forall Γ Δ t ec Σ l, SRule - [Γ > Δ > Σ,, (take_arg_types_as_tree t @@@ (ec::l)) |- [ drop_arg_types_as_tree t @@ (ec::l) ]] - [Γ > Δ > Σ |- [<[ec |- t]> @@ l ]] + [Γ > Δ > Σ,,(take_arg_types_as_tree t @@@ (ec::l)) |- [ drop_arg_types_as_tree t ] @ (ec::l)] + [Γ > Δ > Σ |- [<[ec |- t]> ] @l] | SEsc : forall Γ Δ t ec Σ l, SRule - [Γ > Δ > Σ |- [<[ec |- t]> @@ l ]] - [Γ > Δ > Σ,, (take_arg_types_as_tree t @@@ (ec::l)) |- [ drop_arg_types_as_tree t @@ (ec::l) ]] + [Γ > Δ > Σ |- [<[ec |- t]> ] @l] + [Γ > Δ > Σ,,(take_arg_types_as_tree t @@@ (ec::l)) |- [ drop_arg_types_as_tree t ] @ (ec::l)] . Definition take_arg_types_as_tree' {Γ}(lt:LeveledHaskType Γ ★) := @@ -162,11 +190,9 @@ Section HaskSkolemizer. Definition skolemize_judgment (j:Judg) : Judg := match j with - Γ > Δ > Σ₁ |- Σ₂ => - match getjlev Σ₂ with - | nil => j - | lev => Γ > Δ > Σ₁,,(mapOptionTreeAndFlatten take_arg_types_as_tree' Σ₂) |- mapOptionTree drop_arg_types_as_tree' Σ₂ - end + | Γ > Δ > Σ₁ |- Σ₂ @ nil => j + | Γ > Δ > Σ₁ |- Σ₂ @ lev => + Γ > Δ > Σ₁,,(mapOptionTreeAndFlatten take_arg_types_as_tree Σ₂ @@@ lev) |- mapOptionTree drop_arg_types_as_tree Σ₂ @ lev end. Definition check_hof : forall {Γ}(t:HaskType Γ ★), @@ -182,6 +208,7 @@ Section HaskSkolemizer. left; auto. Defined. + Opaque take_arg_types_as_tree. Definition skolemize_proof : forall {h}{c}, ND Rule h c -> @@ -192,7 +219,7 @@ Section HaskSkolemizer. intros. refine (match X as R in Rule H C with - | RArrange Γ Δ a b x d => let case_RArrange := tt in _ + | RArrange Γ Δ a b x l d => let case_RArrange := tt in _ | RNote Γ Δ Σ τ l n => let case_RNote := tt in _ | RLit Γ Δ l _ => let case_RLit := tt in _ | RVar Γ Δ σ lev => let case_RVar := tt in _ @@ -204,18 +231,19 @@ Section HaskSkolemizer. | RAppCo Γ Δ Σ κ σ₁ σ₂ γ σ lev => let case_RAppCo := tt in _ | RAbsCo Γ Δ Σ κ σ σ₁ σ₂ lev => let case_RAbsCo := tt in _ | RApp Γ Δ Σ₁ Σ₂ tx te lev => let case_RApp := tt in _ - | RLet Γ Δ Σ₁ Σ₂ σ₁ σ₂ lev => let case_RLet := tt in _ - | RJoin Γ p lri m x q => let case_RJoin := tt in _ - | RVoid _ _ => let case_RVoid := tt in _ - | RBrak Γ Δ t ec succ lev => let case_RBrak := tt in _ - | REsc Γ Δ t ec succ lev => let case_REsc := tt in _ + | RCut Γ Δ Σ Σ₁ Σ₁₂ Σ₂ Σ₃ l => let case_RCut := tt in _ + | RLeft Γ Δ Σ₁ Σ₂ Σ l => let case_RLeft := tt in _ + | RRight Γ Δ Σ₁ Σ₂ Σ l => let case_RRight := tt in _ + | RVoid _ _ l => let case_RVoid := tt in _ + | RBrak Γ Δ t ec succ lev => let case_RBrak := tt in _ + | REsc Γ Δ t ec succ lev => let case_REsc := tt in _ | RCase Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt in _ | RLetRec Γ Δ lri x y t => let case_RLetRec := tt in _ end); clear X h c. destruct case_RArrange. simpl. - destruct (getjlev x). + destruct l. apply nd_rule. apply SFlat. apply RArrange. @@ -223,7 +251,7 @@ Section HaskSkolemizer. apply nd_rule. apply SFlat. apply RArrange. - apply RRight. + apply ARight. apply d. destruct case_RBrak. @@ -260,7 +288,7 @@ Section HaskSkolemizer. rewrite H. rewrite H0. simpl. - eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; apply RuCanL ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; apply AuCanL ]. apply nd_rule. apply SFlat. apply RLit. @@ -275,7 +303,7 @@ Section HaskSkolemizer. rewrite H. rewrite H0. simpl. - eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RuCanR ]. + eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply AuCanR ]. apply nd_rule. apply SFlat. apply RVar. @@ -290,23 +318,26 @@ Section HaskSkolemizer. rewrite H. rewrite H0. simpl. - eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RuCanR ]. + eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply AuCanR ]. apply nd_rule. apply SFlat. apply RGlobal. destruct case_RLam. - simpl. destruct lev. - apply nd_rule. - apply SFlat. - apply RLam. - rewrite take_works. + apply nd_rule. + apply SFlat. + simpl. + apply RLam. + simpl. rewrite drop_works. apply nd_rule. - apply SFlat. - apply RArrange. - apply RCossa. + apply SFlat. + apply RArrange. + eapply AComp. + eapply AuAssoc. + eapply ALeft. + apply take_arrange. destruct case_RCast. simpl. @@ -317,23 +348,12 @@ Section HaskSkolemizer. apply γ. apply (Prelude_error "found RCast at level >0"). - destruct case_RJoin. - simpl. - destruct (getjlev x). - destruct (getjlev q). - apply nd_rule. - apply SFlat. - apply RJoin. - apply (Prelude_error "found RJoin at level >0"). - apply (Prelude_error "found RJoin at level >0"). - destruct case_RApp. simpl. destruct lev. apply nd_rule. apply SFlat. apply RApp. - rewrite take_works. rewrite drop_works. set (check_hof tx) as hof_tx. destruct hof_tx; [ apply (Prelude_error "attempt tp apply a higher-order function at depth>0") | idtac ]. @@ -341,51 +361,106 @@ Section HaskSkolemizer. rewrite H. rewrite H0. simpl. - set (@RLet Γ Δ (Σ₂,,take_arg_types_as_tree te @@@ (h :: lev)) Σ₁ (drop_arg_types_as_tree te) tx (h::lev)) as q. - eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RAssoc ]. - eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RExch ]. - eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply q ]. - clear q. + eapply nd_comp. + eapply nd_prod; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ACanR ]. + eapply nd_rule. + eapply SFlat. + eapply RArrange. + eapply ALeft. + eapply take_unarrange. + + eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply AAssoc ]. + eapply nd_comp; [ apply nd_exch | idtac ]. + eapply nd_rule; eapply SFlat; eapply RCut. + + destruct case_RCut. + simpl; destruct l; [ apply nd_rule; apply SFlat; apply RCut | idtac ]. + set (mapOptionTreeAndFlatten take_arg_types_as_tree Σ₃) as Σ₃''. + set (mapOptionTree drop_arg_types_as_tree Σ₃) as Σ₃'''. + set (mapOptionTreeAndFlatten take_arg_types_as_tree Σ₁₂) as Σ₁₂''. + set (mapOptionTree drop_arg_types_as_tree Σ₁₂) as Σ₁₂'''. + destruct (decide_tree_empty (Σ₁₂'' @@@ (h::l))); + [ idtac | apply (Prelude_error "used RCut on a variable with function type") ]. + destruct (eqd_dec Σ₁₂ Σ₁₂'''); [ idtac | apply (Prelude_error "used RCut on a variable with function type") ]. + rewrite <- e. + clear e. + destruct s. + eapply nd_comp. + eapply nd_prod. + eapply nd_rule. + eapply SFlat. + eapply RArrange. + eapply AComp. + eapply ALeft. + eapply arrangeCancelEmptyTree with (q:=x). + apply e. + apply ACanR. + apply nd_id. + eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply AAssoc ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ALeft; eapply AAssoc ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RCut ]. apply nd_prod. + apply nd_id. + eapply nd_rule. + eapply SFlat. + eapply RArrange. + eapply AComp. + eapply AuAssoc. + eapply ALeft. + eapply AComp. + eapply AuAssoc. + eapply ALeft. + eapply AId. + + destruct case_RLeft. + simpl; destruct l; [ apply nd_rule; apply SFlat; apply RLeft | idtac ]. + set (mapOptionTreeAndFlatten take_arg_types_as_tree Σ₂) as Σ₂'. + set (mapOptionTreeAndFlatten take_arg_types_as_tree Σ) as Σ'. + set (mapOptionTree drop_arg_types_as_tree Σ₂) as Σ₂''. + set (mapOptionTree drop_arg_types_as_tree Σ) as Σ''. + destruct (decide_tree_empty (Σ' @@@ (h::l))); + [ idtac | apply (Prelude_error "used RLeft on a variable with function type") ]. + destruct (eqd_dec Σ Σ''); [ idtac | apply (Prelude_error "used RLeft on a variable with function type") ]. + rewrite <- e. + clear Σ'' e. + destruct s. + set (arrangeUnCancelEmptyTree _ _ e) as q. + eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ALeft; eapply ARight; eapply q ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ALeft; eapply AuCanL; eapply q ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply AAssoc ]. apply nd_rule. - apply SFlat. - apply RArrange. - apply RCanR. - eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RAssoc ]. - apply nd_rule; apply SFlat; apply RArrange; apply RLeft; eapply RExch. + eapply SFlat. + eapply RLeft. + + destruct case_RRight. + simpl; destruct l; [ apply nd_rule; apply SFlat; apply RRight | idtac ]. + set (mapOptionTreeAndFlatten take_arg_types_as_tree Σ₂) as Σ₂'. + set (mapOptionTreeAndFlatten take_arg_types_as_tree Σ) as Σ'. + set (mapOptionTree drop_arg_types_as_tree Σ₂) as Σ₂''. + set (mapOptionTree drop_arg_types_as_tree Σ) as Σ''. + destruct (decide_tree_empty (Σ' @@@ (h::l))); + [ idtac | apply (Prelude_error "used RRight on a variable with function type") ]. + destruct (eqd_dec Σ Σ''); [ idtac | apply (Prelude_error "used RRight on a variable with function type") ]. + rewrite <- e. + clear Σ'' e. + destruct s. + set (arrangeUnCancelEmptyTree _ _ e) as q. + eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ALeft; eapply ALeft; eapply q ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ALeft; eapply AuCanR ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply AAssoc ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ALeft; eapply AExch ]. (* yuck *) + eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply AuAssoc ]. + eapply nd_rule. + eapply SFlat. + apply RRight. - destruct case_RLet. + destruct case_RVoid. simpl. - destruct lev. - apply nd_rule. - apply SFlat. - apply RLet. - set (check_hof σ₂) as hof_tx. - destruct hof_tx; [ apply (Prelude_error "attempt to let-bind a higher-order function at depth>0") | idtac ]. - destruct a. - rewrite H. - rewrite H0. - set (@RLet Γ Δ (Σ₁,,(take_arg_types_as_tree σ₁ @@@ (h::lev))) Σ₂ (drop_arg_types_as_tree σ₁) σ₂ (h::lev)) as q. - eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RAssoc ]. - eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; eapply RLeft; apply RExch ]. - eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RCossa ]. - eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply q ]. - clear q. - apply nd_prod. - apply nd_rule. - apply SFlat. - apply RArrange. - apply RCanR. - eapply nd_comp; [ eapply nd_rule; apply SFlat; eapply RArrange; apply RCossa | idtac ]. - eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RAssoc ]. + destruct l. apply nd_rule. apply SFlat. - apply RArrange. - apply RLeft. - eapply RExch. - - destruct case_RVoid. - simpl. + apply RVoid. + eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply AuCanL ]. apply nd_rule. apply SFlat. apply RVoid. @@ -414,16 +489,16 @@ Section HaskSkolemizer. destruct case_RLetRec. simpl. destruct t. - destruct (getjlev (y @@@ nil)). apply nd_rule. apply SFlat. apply (@RLetRec Γ Δ lri x y nil). apply (Prelude_error "RLetRec at depth>0"). - apply (Prelude_error "RLetRec at depth>0"). destruct case_RCase. simpl. apply (Prelude_error "CASE: BIG FIXME"). Defined. + Transparent take_arg_types_as_tree. + End HaskSkolemizer.