Require Import Preamble.
Require Import General.
Require Import NaturalDeduction.
+Require Import NaturalDeductionContext.
Require Import Coq.Strings.String.
Require Import Coq.Lists.List.
| 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.
+*)
+ (* 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.
(* 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
- end.
+ Definition getΓ (j:Judg) := match j with Γ > _ > _ |- _ @ _ => Γ end.
Fixpoint take_trustme {Γ}
(n:nat)
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 take_arg_types_as_tree {Γ}(ht:HaskType Γ ★) : Tree ??(HaskType Γ ★ ) :=
- unleaves
+ unleaves_
(take_trustme
(count_arg_types (ht _ (ite_unit _)))
(fun TV ite => take_arg_types (ht TV ite))).
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 at 1.
- simpl.
- 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).
| 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 Γ ★) :=
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 Γ ★),
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 _
| RGlobal Γ Δ σ l wev => let case_RGlobal := tt in _
| RLam Γ Δ Σ tx te lev => let case_RLam := tt in _
| RCast Γ Δ Σ σ τ lev γ => let case_RCast := tt in _
- | RAbsT Γ Δ Σ κ σ lev => let case_RAbsT := tt in _
+ | RAbsT Γ Δ Σ κ σ lev n => let case_RAbsT := tt in _
| RAppT Γ Δ Σ κ σ τ lev => let case_RAppT := tt in _
| 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.
apply nd_rule.
apply SFlat.
apply RArrange.
- apply RRight.
+ apply ARight.
apply d.
destruct case_RBrak.
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.
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.
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.
simpl.
apply RLam.
simpl.
- rewrite take_works.
rewrite drop_works.
apply nd_rule.
apply SFlat.
apply RArrange.
- apply RCossa.
+ eapply AComp.
+ eapply AuAssoc.
+ eapply ALeft.
+ apply take_arrange.
destruct case_RCast.
simpl.
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 ].
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.
destruct case_RAbsT.
simpl.
- destruct lev; simpl; [ apply nd_rule; apply SFlat; apply (@RAbsT _ _ _ _ _ nil) | idtac ].
+ destruct lev; simpl.
+ apply nd_rule.
+ apply SFlat.
+ apply (@RAbsT Γ Δ Σ κ σ nil n).
apply (Prelude_error "RAbsT at depth>0").
destruct case_RAppCo.
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 (decide_tree_empty (mapOptionTreeAndFlatten take_arg_types_as_tree y @@@ (h :: t)));
+ [ idtac | apply (Prelude_error "used LetRec on a set of bindings involving a function type") ].
+ destruct (eqd_dec y (mapOptionTree drop_arg_types_as_tree y));
+ [ idtac | apply (Prelude_error "used LetRec on a set of bindings involving a function type") ].
+ rewrite <- e.
+ clear e.
+ eapply nd_comp.
+ eapply nd_rule.
+ eapply SFlat.
+ eapply RArrange.
+ eapply ALeft.
+ eapply AComp.
+ eapply ARight.
+ destruct s.
+ apply (arrangeCancelEmptyTree _ _ e).
+ apply ACanL.
+ eapply nd_comp.
+ eapply nd_rule.
+ eapply SFlat.
+ eapply RArrange.
+ eapply AuAssoc.
+ eapply nd_rule.
+ eapply SFlat.
+ eapply RLetRec.
destruct case_RCase.
- simpl.
- apply (Prelude_error "CASE: BIG FIXME").
+ destruct lev; [ idtac | apply (Prelude_error "case at depth >0") ]; simpl.
+ apply nd_rule.
+ apply SFlat.
+ rewrite <- mapOptionTree_compose.
+ assert
+ ((mapOptionTree (fun x => skolemize_judgment (@pcb_judg tc Γ Δ nil tbranches avars (fst x) (snd x))) alts) =
+ (mapOptionTree (fun x => (@pcb_judg tc Γ Δ nil tbranches avars (fst x) (snd x))) alts)).
+ admit.
+ rewrite H.
+ set (@RCase Γ Δ nil tc Σ avars tbranches alts) as q.
+ apply q.
Defined.
+
Transparent take_arg_types_as_tree.
End HaskSkolemizer.
projects / coq-hetmet.git / blobdiff