Require Import HaskStrongTypes.
Require Import HaskProof.
Require Import NaturalDeduction.
-Require Import NaturalDeductionCategory.
-
-Require Import Algebras_ch4.
-Require Import Categories_ch1_3.
-Require Import Functors_ch1_4.
-Require Import Isomorphisms_ch1_5.
-Require Import ProductCategories_ch1_6_1.
-Require Import OppositeCategories_ch1_6_2.
-Require Import Enrichment_ch2_8.
-Require Import Subcategories_ch7_1.
-Require Import NaturalTransformations_ch7_4.
-Require Import NaturalIsomorphisms_ch7_5.
-Require Import BinoidalCategories.
-Require Import PreMonoidalCategories.
-Require Import MonoidalCategories_ch7_8.
-Require Import Coherence_ch7_8.
Require Import HaskStrongTypes.
Require Import HaskStrong.
Require Import HaskProof.
Require Import HaskStrongToProof.
Require Import HaskProofToStrong.
-Require Import ProgrammingLanguage.
-Require Import HaskProgrammingLanguage.
-Require Import PCF.
Open Scope nd_scope.
*)
Section HaskFlattener.
- (* this actually has nothing to do with categories; it shows that proofs [|-A]//[|-B] are one-to-one with []//[A|-B] *)
- (* TODO Lemma hom_functor_full*)
+ Inductive TreeFlags {T:Type} : Tree T -> Type :=
+ | tf_leaf_true : forall x, TreeFlags (T_Leaf x)
+ | tf_leaf_false : forall x, TreeFlags (T_Leaf x)
+ | tf_branch : forall b1 b2, TreeFlags b1 -> TreeFlags b2 -> TreeFlags (b1,,b2).
- (* lemma: if a proof from no hypotheses contains no Brak's or Esc's, then the context contains no variables at level!=0 *)
+ Fixpoint mkFlags {T}(f:T -> bool)(t:Tree T) : TreeFlags t :=
+ match t as T return TreeFlags T with
+ | T_Leaf x => if f x then tf_leaf_true x else tf_leaf_false x
+ | T_Branch b1 b2 => tf_branch _ _ (mkFlags f b1) (mkFlags f b2)
+ end.
+
+ (* take and drop are not exact inverses *)
+
+ (* drop replaces each leaf where the flag is set with a [] *)
+ Fixpoint drop {T}{Σ:Tree ??T}(tf:TreeFlags Σ) : Tree ??T :=
+ match tf with
+ | tf_leaf_true x => []
+ | tf_leaf_false x => Σ
+ | tf_branch b1 b2 tb1 tb2 => (drop tb1),,(drop tb2)
+ end.
+
+ (* take returns only those leaves for which the flag is set; all others are omitted entirely from the tree *)
+ Fixpoint take {T}{Σ:Tree T}(tf:TreeFlags Σ) : ??(Tree T) :=
+ match tf with
+ | tf_leaf_true x => Some Σ
+ | tf_leaf_false x => None
+ | tf_branch b1 b2 tb1 tb2 =>
+ match take tb1 with
+ | None => take tb2
+ | Some b1' => match take tb2 with
+ | None => Some b1'
+ | Some b2' => Some (b1',,b2')
+ end
+ end
+ end.
+
+ Definition maybeTree {T}(t:??(Tree ??T)) : Tree ??T :=
+ match t with
+ | None => []
+ | Some x => x
+ end.
+
+ Definition setNone {T}(b:bool)(f:T -> bool) : ??T -> bool :=
+ fun t =>
+ match t with
+ | None => b
+ | Some x => f x
+ end.
+
+ (* "Arrange" objects are parametric in the type of the leaves of the tree *)
+ Definition arrangeMap :
+ forall {T} (Σ₁ Σ₂:Tree ??T) {R} (f:T -> R),
+ Arrange Σ₁ Σ₂ ->
+ Arrange (mapOptionTree f Σ₁) (mapOptionTree f Σ₂).
+ intros.
+ induction X; simpl.
+ apply RCanL.
+ apply RCanR.
+ apply RuCanL.
+ apply RuCanR.
+ apply RAssoc.
+ apply RCossa.
+ apply RExch.
+ apply RWeak.
+ apply RCont.
+ apply RLeft; auto.
+ apply RRight; auto.
+ eapply RComp; [ apply IHX1 | apply IHX2 ].
+ Defined.
+
+ Definition bnot (b:bool) : bool := if b then false else true.
+
+ Definition swapMiddle {T} (a b c d:Tree ??T) :
+ Arrange ((a,,b),,(c,,d)) ((a,,c),,(b,,d)).
+ eapply RComp.
+ apply RCossa.
+ eapply RComp.
+ eapply RLeft.
+ eapply RComp.
+ eapply RAssoc.
+ eapply RRight.
+ apply RExch.
+ eapply RComp.
+ eapply RLeft.
+ eapply RCossa.
+ eapply RAssoc.
+ Defined.
+
+ Definition arrange :
+ forall {T} (Σ:Tree ??T) (f:T -> bool),
+ Arrange Σ (drop (mkFlags (setNone false f) Σ),,( (drop (mkFlags (setNone false (bnot ○ f)) Σ)))).
+ intros.
+ induction Σ.
+ simpl.
+ destruct a.
+ simpl.
+ destruct (f t); simpl.
+ apply RuCanL.
+ apply RuCanR.
+ simpl.
+ apply RuCanL.
+ simpl in *.
+ eapply RComp; [ idtac | apply swapMiddle ].
+ eapply RComp.
+ eapply RLeft.
+ apply IHΣ2.
+ eapply RRight.
+ apply IHΣ1.
+ Defined.
+
+ Definition arrange' :
+ forall {T} (Σ:Tree ??T) (f:T -> bool),
+ Arrange (drop (mkFlags (setNone false f) Σ),,( (drop (mkFlags (setNone false (bnot ○ f)) Σ)))) Σ.
+ intros.
+ induction Σ.
+ simpl.
+ destruct a.
+ simpl.
+ destruct (f t); simpl.
+ apply RCanL.
+ apply RCanR.
+ simpl.
+ apply RCanL.
+ simpl in *.
+ eapply RComp; [ apply swapMiddle | idtac ].
+ eapply RComp.
+ eapply RLeft.
+ apply IHΣ2.
+ eapply RRight.
+ apply IHΣ1.
+ Defined.
Definition minus' n m :=
match m with
[ clear eqd_dec1 | set (eqd_dec2 (refl_equal _)) as eqd_dec2'; inversion eqd_dec2' ]
end.
- (* The opposite: replace any type which is NOT at level "lev" with None *)
- Definition take_lev {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : Tree ??(HaskType Γ ★) :=
- mapTree (fun t => match t with
- | Some (ttype @@ tlev) => if eqd_dec tlev lev then Some ttype else None
- | _ => None
- end) tt.
+ Fixpoint reduceTree {T}(unit:T)(merge:T -> T -> T)(tt:Tree ??T) : T :=
+ match tt with
+ | T_Leaf None => unit
+ | T_Leaf (Some x) => x
+ | T_Branch b1 b2 => merge (reduceTree unit merge b1) (reduceTree unit merge b2)
+ end.
+
+ Set Printing Width 130.
+
+ Context {unitTy : forall TV, RawHaskType TV ★ }.
+ Context {prodTy : forall TV, RawHaskType TV ★ -> RawHaskType TV ★ -> RawHaskType TV ★ }.
+ Context {gaTy : forall TV, RawHaskType TV ★ -> RawHaskType TV ★ -> RawHaskType TV ★ -> RawHaskType TV ★ }.
+
+ Definition ga_mk_tree {Γ} (tr:Tree ??(HaskType Γ ★)) : HaskType Γ ★ :=
+ fun TV ite => reduceTree (unitTy TV) (prodTy TV) (mapOptionTree (fun x => x TV ite) tr).
+
+ Definition ga_mk {Γ}(ec:HaskType Γ ★ )(ant suc:Tree ??(HaskType Γ ★)) : HaskType Γ ★ :=
+ fun TV ite => gaTy TV (ec TV ite) (ga_mk_tree ant TV ite) (ga_mk_tree suc TV ite).
+
+ Class garrow :=
+ { ga_id : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a a @@ l] ]
+ ; ga_cancelr : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec (a,,[]) a @@ l] ]
+ ; ga_cancell : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec ([],,a) a @@ l] ]
+ ; ga_uncancelr : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a (a,,[]) @@ l] ]
+ ; ga_uncancell : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a ([],,a) @@ l] ]
+ ; ga_assoc : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec ((a,,b),,c) (a,,(b,,c)) @@ l] ]
+ ; ga_unassoc : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec (a,,(b,,c)) ((a,,b),,c) @@ l] ]
+ ; ga_swap : ∀ Γ Δ ec l a b , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec (a,,b) (b,,a) @@ l] ]
+ ; ga_drop : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a [] @@ l] ]
+ ; ga_copy : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a (a,,a) @@ l] ]
+ ; ga_first : ∀ Γ Δ ec l a b x, ND Rule [] [Γ > Δ > [@ga_mk Γ ec a b @@ l] |- [@ga_mk Γ ec (a,,x) (b,,x) @@ l] ]
+ ; ga_second : ∀ Γ Δ ec l a b x, ND Rule [] [Γ > Δ > [@ga_mk Γ ec a b @@ l] |- [@ga_mk Γ ec (x,,a) (x,,b) @@ l] ]
+ ; ga_lit : ∀ Γ Δ ec l lit , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec [] [literalType lit] @@ l] ]
+ ; ga_curry : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [@ga_mk Γ ec (a,,[b]) [c] @@ l] |- [@ga_mk Γ ec a [b ---> c] @@ l] ]
+ ; ga_comp : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [@ga_mk Γ ec a b @@ l],,[@ga_mk Γ ec b c @@ l] |- [@ga_mk Γ ec a c @@ l] ]
+ ; ga_apply : ∀ Γ Δ ec l a a' b c, ND Rule []
+ [Γ > Δ > [@ga_mk Γ ec a [b ---> c] @@ l],,[@ga_mk Γ ec a' [b] @@ l] |- [@ga_mk Γ ec (a,,a') [c] @@ l] ]
+ ; ga_kappa : ∀ Γ Δ ec l a b Σ, ND Rule
+ [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec [] b @@ l] ]
+ [Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ l] ]
+ }.
+ Context `(gar:garrow).
+
+ Notation "a ~~~~> b" := (@ga_mk _ _ a b) (at level 20).
+
+ (*
+ * The story:
+ * - code types <[t]>@c become garrows c () t
+ * - free variables of type t at a level lev deeper than the succedent become garrows c () t
+ * - free variables at the level of the succedent become
+ *)
+ Fixpoint garrowfy_raw_codetypes {TV}{κ}(exp: RawHaskType TV κ) : RawHaskType TV κ :=
+ match exp with
+ | TVar _ x => TVar x
+ | TAll _ y => TAll _ (fun v => garrowfy_raw_codetypes (y v))
+ | TApp _ _ x y => TApp (garrowfy_raw_codetypes x) (garrowfy_raw_codetypes y)
+ | TCon tc => TCon tc
+ | TCoerc _ t1 t2 t => TCoerc (garrowfy_raw_codetypes t1) (garrowfy_raw_codetypes t2)
+ (garrowfy_raw_codetypes t)
+ | TArrow => TArrow
+ | TCode v e => gaTy TV v (unitTy TV) (garrowfy_raw_codetypes e)
+ | TyFunApp tfc kl k lt => TyFunApp tfc kl k (garrowfy_raw_codetypes_list _ lt)
+ end
+ with garrowfy_raw_codetypes_list {TV}(lk:list Kind)(exp:@RawHaskTypeList TV lk) : @RawHaskTypeList TV lk :=
+ match exp in @RawHaskTypeList _ LK return @RawHaskTypeList TV LK with
+ | TyFunApp_nil => TyFunApp_nil
+ | TyFunApp_cons κ kl t rest => TyFunApp_cons _ _ (garrowfy_raw_codetypes t) (garrowfy_raw_codetypes_list _ rest)
+ end.
+ Definition garrowfy_code_types {Γ}{κ}(ht:HaskType Γ κ) : HaskType Γ κ :=
+ fun TV ite =>
+ garrowfy_raw_codetypes (ht TV ite).
+
+ Definition v2t {Γ}(ec:HaskTyVar Γ ★) := fun TV ite => TVar (ec TV ite).
+
+ Fixpoint garrowfy_leveled_code_types' {Γ}(ht:HaskType Γ ★)(lev:HaskLevel Γ) : HaskType Γ ★ :=
+ match lev with
+ | nil => garrowfy_code_types ht
+ | ec::lev' => @ga_mk _ (v2t ec) [] [garrowfy_leveled_code_types' ht lev']
+ end.
+
+ Definition garrowfy_leveled_code_types {Γ}(ht:LeveledHaskType Γ ★) : LeveledHaskType Γ ★ :=
+ match ht with
+ htt @@ lev =>
+ garrowfy_leveled_code_types' htt lev @@ nil
+ end.
+
+ Definition levelMatch {Γ}(lev:HaskLevel Γ) : LeveledHaskType Γ ★ -> bool :=
+ fun t => match t with ttype@@tlev => if eqd_dec tlev lev then true else false end.
(* In a tree of types, replace any type at depth "lev" or greater None *)
- Definition drop_depth {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : Tree ??(LeveledHaskType Γ ★) :=
- mapTree (fun t => match t with
- | Some (ttype @@ tlev) => if eqd_dec tlev lev then None else t
- | _ => t
- end) tt.
+ Definition mkDropFlags {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : TreeFlags tt :=
+ mkFlags (setNone false (levelMatch lev)) tt.
- Lemma drop_depth_lemma : forall Γ (lev:HaskLevel Γ) x, drop_depth lev [x @@ lev] = [].
+ Definition drop_lev {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : Tree ??(LeveledHaskType Γ ★) :=
+ drop (mkDropFlags lev tt).
+
+ (* The opposite: replace any type which is NOT at level "lev" with None *)
+ Definition mkTakeFlags {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : TreeFlags tt :=
+ mkFlags (setNone true (bnot ○ levelMatch lev)) tt.
+
+ Definition take_lev {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : Tree ??(HaskType Γ ★) :=
+ mapOptionTree (fun x => garrowfy_code_types (unlev x)) (drop (mkTakeFlags lev tt)).
+(*
+ mapOptionTree (fun x => garrowfy_code_types (unlev x))
+ (maybeTree (take tt (mkFlags (
+ fun t => match t with
+ | Some (ttype @@ tlev) => if eqd_dec tlev lev then true else false
+ | _ => true
+ end
+ ) tt))).
+*)
+
+ Lemma drop_lev_lemma : forall Γ (lev:HaskLevel Γ) x, drop_lev lev [x @@ lev] = [].
intros; simpl.
Opaque eqd_dec.
- unfold drop_depth.
+ unfold drop_lev.
+ simpl.
+ unfold mkDropFlags.
simpl.
Transparent eqd_dec.
eqd_dec_refl'.
auto.
Qed.
- Lemma drop_depth_lemma_s : forall Γ (lev:HaskLevel Γ) ec x, drop_depth (ec::lev) [x @@ (ec :: lev)] = [].
+ Lemma drop_lev_lemma_s : forall Γ (lev:HaskLevel Γ) ec x, drop_lev (ec::lev) [x @@ (ec :: lev)] = [].
intros; simpl.
Opaque eqd_dec.
- unfold drop_depth.
+ unfold drop_lev.
+ unfold mkDropFlags.
simpl.
Transparent eqd_dec.
eqd_dec_refl'.
auto.
Qed.
- Lemma take_lemma : forall Γ (lev:HaskLevel Γ) x, take_lev lev [x @@ lev] = [x].
+ Lemma take_lemma : forall Γ (lev:HaskLevel Γ) x, take_lev lev [x @@ lev] = [garrowfy_code_types x].
intros; simpl.
Opaque eqd_dec.
unfold take_lev.
+ unfold mkTakeFlags.
simpl.
Transparent eqd_dec.
eqd_dec_refl'.
Ltac drop_simplify :=
match goal with
- | [ |- context[@drop_depth ?G ?L [ ?X @@ ?L ] ] ] =>
- rewrite (drop_depth_lemma G L X)
- | [ |- context[@drop_depth ?G (?E :: ?L) [ ?X @@ (?E :: ?L) ] ] ] =>
- rewrite (drop_depth_lemma_s G L E X)
- | [ |- context[@drop_depth ?G ?N (?A,,?B)] ] =>
- change (@drop_depth G N (A,,B)) with ((@drop_depth G N A),,(@drop_depth G N B))
- | [ |- context[@drop_depth ?G ?N (T_Leaf None)] ] =>
- change (@drop_depth G N (T_Leaf (@None (LeveledHaskType G ★)))) with (T_Leaf (@None (LeveledHaskType G ★)))
+ | [ |- context[@drop_lev ?G ?L [ ?X @@ ?L ] ] ] =>
+ rewrite (drop_lev_lemma G L X)
+ | [ |- context[@drop_lev ?G (?E :: ?L) [ ?X @@ (?E :: ?L) ] ] ] =>
+ rewrite (drop_lev_lemma_s G L E X)
+ | [ |- context[@drop_lev ?G ?N (?A,,?B)] ] =>
+ change (@drop_lev G N (A,,B)) with ((@drop_lev G N A),,(@drop_lev G N B))
+ | [ |- context[@drop_lev ?G ?N (T_Leaf None)] ] =>
+ change (@drop_lev G N (T_Leaf (@None (LeveledHaskType G ★)))) with (T_Leaf (@None (LeveledHaskType G ★)))
end.
Ltac take_simplify :=
change (@take_lev G N (T_Leaf (@None (LeveledHaskType G ★)))) with (T_Leaf (@None (LeveledHaskType G ★)))
end.
- Fixpoint reduceTree {T}(unit:T)(merge:T -> T -> T)(tt:Tree ??T) : T :=
- match tt with
- | T_Leaf None => unit
- | T_Leaf (Some x) => x
- | T_Branch b1 b2 => merge (reduceTree unit merge b1) (reduceTree unit merge b2)
- end.
-
- Set Printing Width 130.
-
- Context {unitTy : forall TV, RawHaskType TV ★ }.
- Context {prodTy : forall TV, RawHaskType TV (★ ⇛ ★ ⇛ ★) }.
- Context {gaTy : forall TV, RawHaskType TV (★ ⇛ ★ ⇛ ★ ⇛ ★)}.
-
- Definition ga_tree := fun TV tr => reduceTree (unitTy TV) (fun t1 t2 => TApp (TApp (prodTy TV) t1) t2) tr.
- Definition ga' := fun TV ec ant' suc' => TApp (TApp (TApp (gaTy TV) ec) (ga_tree TV ant')) (ga_tree TV suc').
- Definition ga {Γ} : HaskType Γ ★ -> Tree ??(HaskType Γ ★) -> Tree ??(HaskType Γ ★) -> HaskType Γ ★ :=
- fun ec ant suc =>
- fun TV ite =>
- let ant' := mapOptionTree (fun x => x TV ite) ant in
- let suc' := mapOptionTree (fun x => x TV ite) suc in
- ga' TV (ec TV ite) ant' suc'.
-
- Class garrow :=
- { ga_id : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga Γ ec a a @@ l] ]
- ; ga_cancelr : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga Γ ec (a,,[]) a @@ l] ]
- ; ga_cancell : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga Γ ec ([],,a) a @@ l] ]
- ; ga_uncancelr : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga Γ ec a (a,,[]) @@ l] ]
- ; ga_uncancell : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga Γ ec a ([],,a) @@ l] ]
- ; ga_assoc : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [] |- [@ga Γ ec ((a,,b),,c) (a,,(b,,c)) @@ l] ]
- ; ga_unassoc : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [] |- [@ga Γ ec (a,,(b,,c)) ((a,,b),,c) @@ l] ]
- ; ga_swap : ∀ Γ Δ ec l a b , ND Rule [] [Γ > Δ > [] |- [@ga Γ ec (a,,b) (b,,a) @@ l] ]
- ; ga_drop : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga Γ ec a [] @@ l] ]
- ; ga_copy : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga Γ ec a (a,,a) @@ l] ]
- ; ga_first : ∀ Γ Δ ec l a b x, ND Rule [] [Γ > Δ > [@ga Γ ec a b @@ l] |- [@ga Γ ec (a,,x) (b,,x) @@ l] ]
- ; ga_second : ∀ Γ Δ ec l a b x, ND Rule [] [Γ > Δ > [@ga Γ ec a b @@ l] |- [@ga Γ ec (x,,a) (x,,b) @@ l] ]
- ; ga_lit : ∀ Γ Δ ec l lit , ND Rule [] [Γ > Δ > [] |- [@ga Γ ec [] [literalType lit] @@ l] ]
- ; ga_curry : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [@ga Γ ec (a,,[b]) [c] @@ l] |- [@ga Γ ec a [b ---> c] @@ l] ]
- ; ga_comp : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [@ga Γ ec a b @@ l],,[@ga Γ ec b c @@ l] |- [@ga Γ ec a c @@ l] ]
- ; ga_apply : ∀ Γ Δ ec l a a' b c, ND Rule []
- [Γ > Δ > [@ga Γ ec a [b ---> c] @@ l],,[@ga Γ ec a' [b] @@ l] |- [@ga Γ ec (a,,a') [c] @@ l] ]
- ; ga_kappa : ∀ Γ Δ ec l a b Σ, ND Rule
- [Γ > Δ > Σ,,[@ga Γ ec [] a @@ l] |- [@ga Γ ec [] b @@ l] ]
- [Γ > Δ > Σ |- [@ga Γ ec a b @@ l] ]
- }.
- Context `(gar:garrow).
+ Axiom literal_types_unchanged : forall Γ l, garrowfy_code_types (literalType l) = literalType(Γ:=Γ) l.
- Notation "a ~~~~> b" := (@ga _ _ a b) (at level 20).
-
- (*
- * The story:
- * - code types <[t]>@c become garrows c () t
- * - free variables of type t at a level lev deeper than the succedent become garrows c () t
- * - free variables at the level of the succedent become
- *)
- Fixpoint garrowfy_raw_codetypes {TV}{κ}(depth:nat)(exp: RawHaskType TV κ) : RawHaskType TV κ :=
- match exp with
- | TVar _ x => TVar x
- | TAll _ y => TAll _ (fun v => garrowfy_raw_codetypes depth (y v))
- | TApp _ _ x y => TApp (garrowfy_raw_codetypes depth x) (garrowfy_raw_codetypes depth y)
- | TCon tc => TCon tc
- | TCoerc _ t1 t2 t => TCoerc (garrowfy_raw_codetypes depth t1) (garrowfy_raw_codetypes depth t2)
- (garrowfy_raw_codetypes depth t)
- | TArrow => TArrow
- | TCode v e => match depth with
- | O => ga' TV v [] [(*garrowfy_raw_codetypes depth*) e]
- | (S depth') => TCode v (garrowfy_raw_codetypes depth' e)
- end
- | TyFunApp tfc lt => TyFunApp tfc (garrowfy_raw_codetypes_list _ depth lt)
- end
- with garrowfy_raw_codetypes_list {TV}(lk:list Kind)(depth:nat)(exp:@RawHaskTypeList TV lk) : @RawHaskTypeList TV lk :=
- match exp in @RawHaskTypeList _ LK return @RawHaskTypeList TV LK with
- | TyFunApp_nil => TyFunApp_nil
- | TyFunApp_cons κ kl t rest => TyFunApp_cons _ _ (garrowfy_raw_codetypes depth t) (garrowfy_raw_codetypes_list _ depth rest)
- end.
- Definition garrowfy_code_types {Γ}{κ}(n:nat)(ht:HaskType Γ κ) : HaskType Γ κ :=
- fun TV ite =>
- garrowfy_raw_codetypes n (ht TV ite).
- Definition garrowfy_leveled_code_types {Γ}(n:nat)(ht:LeveledHaskType Γ ★) : LeveledHaskType Γ ★ :=
- match ht with htt @@ htlev => garrowfy_code_types (minus' n (length htlev)) htt @@ htlev end.
-
- Axiom literal_types_unchanged : forall n Γ l, garrowfy_code_types n (literalType l) = literalType(Γ:=Γ) l.
-
- Axiom flatten_coercion : forall n Γ Δ κ (σ τ:HaskType Γ κ) (γ:HaskCoercion Γ Δ (σ ∼∼∼ τ)),
- HaskCoercion Γ Δ (garrowfy_code_types n σ ∼∼∼ garrowfy_code_types n τ).
+ Axiom flatten_coercion : forall Γ Δ κ (σ τ:HaskType Γ κ) (γ:HaskCoercion Γ Δ (σ ∼∼∼ τ)),
+ HaskCoercion Γ Δ (garrowfy_code_types σ ∼∼∼ garrowfy_code_types τ).
(* This tries to assign a single level to the entire succedent of a judgment. If the succedent has types from different
* levels (should not happen) it just picks one; if the succedent has no non-None leaves (also should not happen) it
end
end.
- Definition v2t {Γ}(ec:HaskTyVar Γ ★) := fun TV ite => TVar (ec TV ite).
+ Definition unlev' {Γ} (x:LeveledHaskType Γ ★) :=
+ garrowfy_code_types (unlev x).
(* "n" is the maximum depth remaining AFTER flattening *)
- Definition flatten_judgment (n:nat)(j:Judg) :=
+ Definition flatten_judgment (j:Judg) :=
match j as J return Judg with
Γ > Δ > ant |- suc =>
- match (match getjlev suc with
- | nil => inl _ tt
- | (ec::lev') => if eqd_dec (length lev') n
- (* If the judgment's level is the deepest in the proof, flatten it by turning
- * all antecedent variables at this level into None's, garrowfying any other
- * antecedent variables (from other levels) at the same depth, and turning the
- * succedent into a garrow type *)
- then inr _ (Γ > Δ > mapOptionTree (garrowfy_leveled_code_types n) (drop_depth (ec::lev') ant)
- |- [ga (v2t ec) (take_lev (ec::lev') ant) (mapOptionTree unlev suc) @@ lev'])
- else inl _ tt
- end) with
-
- (* otherwise, just garrowfy all code types of the specified depth, throughout the judgment *)
- | inl tt => Γ > Δ > mapOptionTree (garrowfy_leveled_code_types n) ant |- mapOptionTree (garrowfy_leveled_code_types n) suc
- | inr r => r
+ match getjlev suc with
+ | nil => Γ > Δ > mapOptionTree garrowfy_leveled_code_types ant
+ |- mapOptionTree garrowfy_leveled_code_types suc
+
+ | (ec::lev') => Γ > Δ > mapOptionTree garrowfy_leveled_code_types (drop_lev (ec::lev') ant)
+ |- [ga_mk (v2t ec)
+ (take_lev (ec::lev') ant)
+ (mapOptionTree unlev' suc) (* we know the level of all of suc *)
+ @@ nil]
end
end.
- Definition boost : forall Γ Δ ant x y,
- ND Rule [] [ Γ > Δ > x |- y ] ->
- ND Rule [ Γ > Δ > ant |- x ] [ Γ > Δ > ant |- y ].
- admit.
+ Definition boost : forall Γ Δ ant x y {lev},
+ ND Rule [] [ Γ > Δ > [x@@lev] |- [y@@lev] ] ->
+ ND Rule [ Γ > Δ > ant |- [x@@lev] ] [ Γ > Δ > ant |- [y@@lev] ].
+ intros.
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
+ eapply nd_comp; [ idtac | eapply nd_rule; apply (@RLet Γ Δ [] ant y x lev) ].
+ eapply nd_comp; [ apply nd_rlecnac | idtac ].
+ apply nd_prod.
+ apply nd_id.
+ eapply nd_comp.
+ apply X.
+ eapply nd_rule.
+ eapply RArrange.
+ apply RuCanL.
+ Defined.
+
+ Definition postcompose' : ∀ Γ Δ ec lev a b c Σ,
+ ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ lev] ] ->
+ ND Rule [] [ Γ > Δ > Σ,,[@ga_mk Γ ec b c @@ lev] |- [@ga_mk Γ ec a c @@ lev] ].
+ intros.
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
+ eapply nd_comp; [ idtac | eapply nd_rule; apply (@RLet Γ Δ [@ga_mk _ ec b c @@lev] Σ (@ga_mk _ ec a c) (@ga_mk _ ec a b) lev) ].
+ eapply nd_comp; [ apply nd_llecnac | idtac ].
+ apply nd_prod.
+ apply X.
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RExch ].
+ apply ga_comp.
Defined.
- Definition postcompose : ∀ Γ Δ ec lev a b c,
- ND Rule [] [ Γ > Δ > [] |- [@ga Γ ec a b @@ lev] ] ->
- ND Rule [] [ Γ > Δ > [@ga Γ ec b c @@ lev] |- [@ga Γ ec a c @@ lev] ].
- admit.
+ Definition precompose' : ∀ Γ Δ ec lev a b c Σ,
+ ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec b c @@ lev] ] ->
+ ND Rule [] [ Γ > Δ > Σ,,[@ga_mk Γ ec a b @@ lev] |- [@ga_mk Γ ec a c @@ lev] ].
+ intros.
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
+ eapply nd_comp; [ idtac | eapply nd_rule; apply (@RLet Γ Δ [@ga_mk _ ec a b @@lev] Σ (@ga_mk _ ec a c) (@ga_mk _ ec b c) lev) ].
+ eapply nd_comp; [ apply nd_llecnac | idtac ].
+ apply nd_prod.
+ apply X.
+ apply ga_comp.
Defined.
- Definition seq : ∀ Γ Δ lev a b,
- ND Rule [] [ Γ > Δ > [] |- [a @@ lev] ] ->
- ND Rule [] [ Γ > Δ > [] |- [b @@ lev] ] ->
- ND Rule [] [ Γ > Δ > [] |- [a @@ lev],,[b @@ lev] ].
- admit.
+ Definition postcompose : ∀ Γ Δ ec lev a b c,
+ ND Rule [] [ Γ > Δ > [] |- [@ga_mk Γ ec a b @@ lev] ] ->
+ ND Rule [] [ Γ > Δ > [@ga_mk Γ ec b c @@ lev] |- [@ga_mk Γ ec a c @@ lev] ].
+ intros.
+ eapply nd_comp.
+ apply postcompose'.
+ apply X.
+ apply nd_rule.
+ apply RArrange.
+ apply RCanL.
Defined.
+ Definition firstify : ∀ Γ Δ ec lev a b c Σ,
+ ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ lev] ] ->
+ ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec (a,,c) (b,,c) @@ lev] ].
+ intros.
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
+ eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
+ eapply nd_comp; [ apply nd_llecnac | idtac ].
+ apply nd_prod.
+ apply X.
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RuCanL ].
+ apply ga_first.
+ Defined.
+
+ Definition secondify : ∀ Γ Δ ec lev a b c Σ,
+ ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ lev] ] ->
+ ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec (c,,a) (c,,b) @@ lev] ].
+ intros.
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
+ eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
+ eapply nd_comp; [ apply nd_llecnac | idtac ].
+ apply nd_prod.
+ apply X.
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RuCanL ].
+ apply ga_second.
+ Defined.
+
Lemma ga_unkappa : ∀ Γ Δ ec l a b Σ,
ND Rule
- [Γ > Δ > Σ |- [@ga Γ ec a b @@ l] ]
- [Γ > Δ > Σ,,[@ga Γ ec [] a @@ l] |- [@ga Γ ec [] b @@ l] ].
+ [Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ l] ]
+ [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec [] b @@ l] ].
intros.
set (ga_comp Γ Δ ec l [] a b) as q.
set (@RLet Γ Δ) as q'.
- set (@RLet Γ Δ [@ga _ ec [] a @@ l] Σ (@ga _ ec [] b) (@ga _ ec a b) l) as q''.
+ set (@RLet Γ Δ [@ga_mk _ ec [] a @@ l] Σ (@ga_mk _ ec [] b) (@ga_mk _ ec a b) l) as q''.
eapply nd_comp.
Focus 2.
eapply nd_rule.
(*
Notation "` x" := (take_lev _ x) (at level 20).
Notation "`` x" := (mapOptionTree unlev x) (at level 20).
- Notation "``` x" := (drop_depth _ x) (at level 20).
+ Notation "``` x" := (drop_lev _ x) (at level 20).
*)
Definition garrowfy_arrangement' :
forall Γ (Δ:CoercionEnv Γ)
(ec:HaskTyVar Γ ★) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2),
- ND Rule [] [Γ > Δ > [] |- [@ga _ (v2t ec) (take_lev (ec :: lev) ant2) (take_lev (ec :: lev) ant1) @@ lev] ].
+ ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec) (take_lev (ec :: lev) ant2) (take_lev (ec :: lev) ant1) @@ nil] ].
intros Γ Δ ec lev.
refine (fix garrowfy ant1 ant2 (r:Arrange ant1 ant2):
- ND Rule [] [Γ > Δ > [] |- [@ga _ (v2t ec) (take_lev (ec :: lev) ant2) (take_lev (ec :: lev) ant1) @@ lev]] :=
+ ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec) (take_lev (ec :: lev) ant2) (take_lev (ec :: lev) ant1) @@ nil]] :=
match r as R in Arrange A B return
- ND Rule [] [Γ > Δ > [] |- [@ga _ (v2t ec) (take_lev (ec :: lev) B) (take_lev (ec :: lev) A) @@ lev]]
+ ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec) (take_lev (ec :: lev) B) (take_lev (ec :: lev) A) @@ nil]]
with
| RCanL a => let case_RCanL := tt in ga_uncancell _ _ _ _ _
| RCanR a => let case_RCanR := tt in ga_uncancelr _ _ _ _ _
| RCont a => let case_RCont := tt in ga_copy _ _ _ _ _
| RLeft a b c r' => let case_RLeft := tt in garrowfy _ _ r' ;; boost _ _ _ _ _ (ga_second _ _ _ _ _ _ _)
| RRight a b c r' => let case_RRight := tt in garrowfy _ _ r' ;; boost _ _ _ _ _ (ga_first _ _ _ _ _ _ _)
- | RComp a b c r1 r2 => let case_RComp := tt in (fun r1' r2' => _) (garrowfy _ _ r1) (garrowfy _ _ r2)
+ | RComp c b a r1 r2 => let case_RComp := tt in (fun r1' r2' => _) (garrowfy _ _ r1) (garrowfy _ _ r2)
end); clear garrowfy; repeat take_simplify; repeat drop_simplify; intros.
destruct case_RComp.
- refine ( _ ;; boost _ _ _ _ _ (ga_comp _ _ _ _ _ _ _)).
- apply seq.
+ set (take_lev (ec :: lev) a) as a' in *.
+ set (take_lev (ec :: lev) b) as b' in *.
+ set (take_lev (ec :: lev) c) as c' in *.
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanL ].
+ eapply nd_comp; [ idtac | eapply nd_rule; apply
+ (@RLet Γ Δ [] [] (@ga_mk _ (v2t ec) a' c') (@ga_mk _ (v2t ec) a' b')) ].
+ eapply nd_comp; [ apply nd_llecnac | idtac ].
+ apply nd_prod.
apply r2'.
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RuCanL ].
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanR ].
+ eapply nd_comp; [ idtac | eapply nd_rule; apply
+ (@RLet Γ Δ [@ga_mk _ (v2t ec) a' b' @@ _] [] (@ga_mk _ (v2t ec) a' c') (@ga_mk _ (v2t ec) b' c'))].
+ eapply nd_comp; [ apply nd_llecnac | idtac ].
+ eapply nd_prod.
apply r1'.
+ apply ga_comp.
Defined.
Definition garrowfy_arrangement :
forall Γ (Δ:CoercionEnv Γ) n
(ec:HaskTyVar Γ ★) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2) succ,
ND Rule
- [Γ > Δ > mapOptionTree (garrowfy_leveled_code_types ((length lev))) (drop_depth n ant1)
- |- [@ga _ (v2t ec) (take_lev (ec :: lev) ant1) (mapOptionTree unlev succ) @@ lev]]
- [Γ > Δ > mapOptionTree (garrowfy_leveled_code_types ((length lev))) (drop_depth n ant2)
- |- [@ga _ (v2t ec) (take_lev (ec :: lev) ant2) (mapOptionTree unlev succ) @@ lev]].
+ [Γ > Δ > mapOptionTree (garrowfy_leveled_code_types ) (drop_lev n ant1)
+ |- [@ga_mk _ (v2t ec) (take_lev (ec :: lev) ant1) (mapOptionTree (unlev' ) succ) @@ nil]]
+ [Γ > Δ > mapOptionTree (garrowfy_leveled_code_types ) (drop_lev n ant2)
+ |- [@ga_mk _ (v2t ec) (take_lev (ec :: lev) ant2) (mapOptionTree (unlev' ) succ) @@ nil]].
intros.
refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ (garrowfy_arrangement' Γ Δ ec lev ant1 ant2 r)))).
apply nd_rule.
apply RArrange.
refine ((fix garrowfy ant1 ant2 (r:Arrange ant1 ant2) :=
match r as R in Arrange A B return
- Arrange (mapOptionTree (garrowfy_leveled_code_types ((length lev))) (drop_depth _ A))
- (mapOptionTree (garrowfy_leveled_code_types ((length lev))) (drop_depth _ B)) with
+ Arrange (mapOptionTree (garrowfy_leveled_code_types ) (drop_lev _ A))
+ (mapOptionTree (garrowfy_leveled_code_types ) (drop_lev _ B)) with
| RCanL a => let case_RCanL := tt in RCanL _
| RCanR a => let case_RCanR := tt in RCanR _
| RuCanL a => let case_RuCanL := tt in RuCanL _
Defined.
Definition flatten_arrangement :
- forall n Γ Δ ant1 ant2 succ (r:Arrange ant1 ant2),
- ND Rule (mapOptionTree (flatten_judgment n) [Γ > Δ > ant1 |- succ])
- (mapOptionTree (flatten_judgment n) [Γ > Δ > ant2 |- succ]).
+ forall Γ Δ ant1 ant2 succ (r:Arrange ant1 ant2),
+ ND Rule (mapOptionTree (flatten_judgment ) [Γ > Δ > ant1 |- succ])
+ (mapOptionTree (flatten_judgment ) [Γ > Δ > ant2 |- succ]).
intros.
simpl.
set (getjlev succ) as succ_lev.
apply RRight; auto.
eapply RComp; [ apply IHr1 | apply IHr2 ].
- set (Peano_dec.eq_nat_dec (Datatypes.length succ_lev) n) as lev_is_n.
- assert (lev_is_n=Peano_dec.eq_nat_dec (Datatypes.length succ_lev) n).
- reflexivity.
- destruct lev_is_n.
- rewrite <- e.
- apply garrowfy_arrangement.
+ apply garrowfy_arrangement.
apply r.
- auto.
- apply nd_rule.
- apply RArrange.
- induction r; simpl.
- apply RCanL.
- apply RCanR.
- apply RuCanL.
- apply RuCanR.
- apply RAssoc.
- apply RCossa.
- apply RExch.
- apply RWeak.
- apply RCont.
- apply RLeft; auto.
- apply RRight; auto.
- eapply RComp; [ apply IHr1 | apply IHr2 ].
Defined.
+ Definition ga_join Γ Δ Σ₁ Σ₂ a b ec :
+ ND Rule [] [Γ > Δ > Σ₁ |- [@ga_mk _ ec [] a @@ nil]] ->
+ ND Rule [] [Γ > Δ > Σ₂ |- [@ga_mk _ ec [] b @@ nil]] ->
+ ND Rule [] [Γ > Δ > Σ₁,,Σ₂ |- [@ga_mk _ ec [] (a,,b) @@ nil]].
+ intro pfa.
+ intro pfb.
+ apply secondify with (c:=a) in pfb.
+ eapply nd_comp.
+ Focus 2.
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
+ eapply nd_comp; [ eapply nd_llecnac | idtac ].
+ eapply nd_prod.
+ apply pfb.
+ clear pfb.
+ apply postcompose'.
+ eapply nd_comp.
+ apply pfa.
+ clear pfa.
+ apply boost.
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
+ apply precompose'.
+ apply ga_uncancelr.
+ apply nd_id.
+ Defined.
+
Definition arrange_brak : forall Γ Δ ec succ t,
- ND Rule
- [Γ > Δ >
- mapOptionTree (garrowfy_leveled_code_types 0) (drop_depth (ec :: nil) succ),,
- [(@ga _ (v2t ec) [] (take_lev (ec :: nil) succ)) @@ nil] |-
- [(@ga _ (v2t ec) [] [t]) @@ nil]]
- [Γ > Δ > mapOptionTree (garrowfy_leveled_code_types 0) succ |- [(@ga _ (v2t ec) [] [t]) @@ nil]].
- admit.
+ ND Rule
+ [Γ > Δ > mapOptionTree (garrowfy_leveled_code_types ) (drop_lev (ec :: nil) succ),,
+ [(@ga_mk _ (v2t ec) [] (take_lev (ec :: nil) succ)) @@ nil] |- [(@ga_mk _ (v2t ec) [] [garrowfy_code_types t]) @@ nil]]
+ [Γ > Δ > mapOptionTree (garrowfy_leveled_code_types ) succ |- [(@ga_mk _ (v2t ec) [] [garrowfy_code_types t]) @@ nil]].
+ intros.
+ unfold drop_lev.
+ set (@arrange' _ succ (levelMatch (ec::nil))) as q.
+ set (arrangeMap _ _ garrowfy_leveled_code_types q) as y.
+ eapply nd_comp.
+ Focus 2.
+ eapply nd_rule.
+ eapply RArrange.
+ apply y.
+ idtac.
+ clear y q.
+ simpl.
+ eapply nd_comp; [ apply nd_llecnac | idtac ].
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
+ apply nd_prod.
+ Focus 2.
+ apply nd_id.
+ idtac.
+ induction succ; try destruct a; simpl.
+ unfold take_lev.
+ unfold mkTakeFlags.
+ unfold mkFlags.
+ unfold bnot.
+ simpl.
+ destruct l as [t' lev'].
+ destruct lev' as [|ec' lev'].
+ simpl.
+ apply ga_id.
+ unfold levelMatch.
+ set (@eqd_dec (HaskLevel Γ) (haskLevelEqDecidable Γ) (ec' :: lev') (ec :: nil)) as q.
+ destruct q.
+ inversion e; subst.
+ simpl.
+ apply nd_rule.
+ apply RVar.
+ simpl.
+ apply ga_id.
+ apply ga_id.
+ unfold take_lev.
+ simpl.
+ apply ga_join.
+ apply IHsucc1.
+ apply IHsucc2.
Defined.
Definition arrange_esc : forall Γ Δ ec succ t,
- ND Rule
- [Γ > Δ > mapOptionTree (garrowfy_leveled_code_types 0) succ |- [(@ga _ (v2t ec) [] [t]) @@ nil]]
- [Γ > Δ >
- mapOptionTree (garrowfy_leveled_code_types 0) (drop_depth (ec :: nil) succ),,
- [(@ga _ (v2t ec) [] (take_lev (ec :: nil) succ)) @@ nil] |- [(@ga _ (v2t ec) [] [t]) @@ nil]].
- admit.
- Defined.
+ ND Rule
+ [Γ > Δ > mapOptionTree (garrowfy_leveled_code_types ) succ |- [(@ga_mk _ (v2t ec) [] [garrowfy_code_types t]) @@ nil]]
+ [Γ > Δ > mapOptionTree (garrowfy_leveled_code_types ) (drop_lev (ec :: nil) succ),,
+ [(@ga_mk _ (v2t ec) [] (take_lev (ec :: nil) succ)) @@ nil] |- [(@ga_mk _ (v2t ec) [] [garrowfy_code_types t]) @@ nil]].
+ intros.
+ unfold drop_lev.
+ set (@arrange _ succ (levelMatch (ec::nil))) as q.
+ set (arrangeMap _ _ garrowfy_leveled_code_types q) as y.
+ eapply nd_comp.
+ eapply nd_rule.
+ eapply RArrange.
+ apply y.
+ idtac.
+ clear y q.
+
+ induction succ.
+ destruct a.
+ destruct l.
+ simpl.
+ unfold mkDropFlags; simpl.
+ unfold take_lev.
+ unfold mkTakeFlags.
+ simpl.
+ destruct (General.list_eq_dec h0 (ec :: nil)).
+ simpl.
+ unfold garrowfy_leveled_code_types'.
+ rewrite e.
+ apply nd_id.
+ simpl.
+ apply nd_rule.
+ apply RArrange.
+ apply RLeft.
+ apply RWeak.
+ simpl.
+ apply nd_rule.
+ unfold take_lev.
+ simpl.
+ apply RArrange.
+ apply RLeft.
+ apply RWeak.
+ apply (Prelude_error "escapifying code with multi-leaf antecedents is not supported").
+ Defined.
Lemma mapOptionTree_distributes
: forall T R (a b:Tree ??T) (f:T->R),
reflexivity.
Qed.
- Lemma garrowfy_commutes_with_substT :
- forall n κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★) (τ:HaskType Γ κ),
- garrowfy_code_types n (substT σ τ) = substT (fun TV ite v => garrowfy_raw_codetypes n (σ TV ite v))
- (garrowfy_code_types n τ).
- admit.
- Qed.
-
- Lemma garrowfy_commutes_with_HaskTAll :
- forall n κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★),
- garrowfy_code_types n (HaskTAll κ σ) = HaskTAll κ (fun TV ite v => garrowfy_raw_codetypes n (σ TV ite v)).
- admit.
- Qed.
-
- Lemma garrowfy_commutes_with_HaskTApp :
- forall n κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★),
- garrowfy_code_types n (HaskTApp (weakF σ) (FreshHaskTyVar κ)) =
- HaskTApp (weakF (fun TV ite v => garrowfy_raw_codetypes n (σ TV ite v))) (FreshHaskTyVar κ).
- admit.
- Qed.
-
- Lemma garrowfy_commutes_with_weakLT : forall (Γ:TypeEnv) κ n t,
- garrowfy_leveled_code_types n (weakLT(Γ:=Γ)(κ:=κ) t) = weakLT(Γ:=Γ)(κ:=κ) (garrowfy_leveled_code_types n t).
- admit.
- Qed.
+ Axiom garrowfy_commutes_with_substT :
+ forall κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★) (τ:HaskType Γ κ),
+ garrowfy_code_types (substT σ τ) = substT (fun TV ite v => garrowfy_raw_codetypes (σ TV ite v))
+ (garrowfy_code_types τ).
+
+ Axiom garrowfy_commutes_with_HaskTAll :
+ forall κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★),
+ garrowfy_code_types (HaskTAll κ σ) = HaskTAll κ (fun TV ite v => garrowfy_raw_codetypes (σ TV ite v)).
+
+ Axiom garrowfy_commutes_with_HaskTApp :
+ forall κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★),
+ garrowfy_code_types (HaskTApp (weakF σ) (FreshHaskTyVar κ)) =
+ HaskTApp (weakF (fun TV ite v => garrowfy_raw_codetypes (σ TV ite v))) (FreshHaskTyVar κ).
+
+ Axiom garrowfy_commutes_with_weakLT : forall (Γ:TypeEnv) κ t,
+ garrowfy_leveled_code_types (weakLT(Γ:=Γ)(κ:=κ) t) = weakLT(Γ:=Γ)(κ:=κ) (garrowfy_leveled_code_types t).
+
+ Axiom globals_do_not_have_code_types : forall (Γ:TypeEnv) (g:Global Γ) v,
+ garrowfy_code_types (g v) = g v.
+
+ Definition decide_tree_empty : forall {T:Type}(t:Tree ??T),
+ sum { q:Tree unit & t = mapTree (fun _ => None) q } unit.
+ intro T.
+ refine (fix foo t :=
+ match t with
+ | T_Leaf x => _
+ | T_Branch b1 b2 => let b1' := foo b1 in let b2' := foo b2 in _
+ end).
+ intros.
+ destruct x.
+ right; apply tt.
+ left.
+ exists (T_Leaf tt).
+ auto.
+ destruct b1'.
+ destruct b2'.
+ destruct s.
+ destruct s0.
+ subst.
+ left.
+ exists (x,,x0).
+ reflexivity.
+ right; auto.
+ right; auto.
+ Defined.
+
Definition flatten_proof :
- forall n {h}{c},
+ forall {h}{c},
ND Rule h c ->
- ND Rule (mapOptionTree (flatten_judgment n) h) (mapOptionTree (flatten_judgment n) c).
+ ND Rule (mapOptionTree (flatten_judgment ) h) (mapOptionTree (flatten_judgment ) c).
intros.
eapply nd_map'; [ idtac | apply X ].
clear h c X.
end); clear X h c.
destruct case_RArrange.
- apply (flatten_arrangement n Γ Δ a b x d).
+ apply (flatten_arrangement Γ Δ a b x d).
destruct case_RBrak.
simpl.
- destruct (Peano_dec.eq_nat_dec (Datatypes.length lev) n).
destruct lev.
- simpl.
- simpl.
- destruct n.
- change ([garrowfy_code_types 0 (<[ ec |- t ]>) @@ nil])
- with ([ga (v2t ec) [] [t] @@ nil]).
- refine (ga_unkappa Γ Δ (v2t ec) nil (take_lev (ec::nil) succ) [t]
- (mapOptionTree (garrowfy_leveled_code_types 0) (drop_depth (ec::nil) succ)) ;; _).
+ change ([garrowfy_code_types (<[ ec |- t ]>) @@ nil])
+ with ([ga_mk (v2t ec) [] [garrowfy_code_types t] @@ nil]).
+ refine (ga_unkappa Γ Δ (v2t ec) nil (take_lev (ec::nil) succ) _
+ (mapOptionTree (garrowfy_leveled_code_types) (drop_lev (ec::nil) succ)) ;; _ ).
apply arrange_brak.
- inversion e.
- apply (Prelude_error "found Brak at depth >0").
- apply (Prelude_error "found Brak at depth >0").
+ apply (Prelude_error "found Brak at depth >0 (a)").
destruct case_REsc.
simpl.
- destruct (Peano_dec.eq_nat_dec (Datatypes.length lev) n).
destruct lev.
simpl.
- destruct n.
- change ([garrowfy_code_types 0 (<[ ec |- t ]>) @@ nil])
- with ([ga (v2t ec) [] [t] @@ nil]).
- refine (_ ;; ga_kappa Γ Δ (v2t ec) nil (take_lev (ec::nil) succ) [t]
- (mapOptionTree (garrowfy_leveled_code_types 0) (drop_depth (ec::nil) succ))).
- apply arrange_esc.
- inversion e.
- apply (Prelude_error "found Esc at depth >0").
- apply (Prelude_error "found Esc at depth >0").
+ change ([garrowfy_code_types (<[ ec |- t ]>) @@ nil])
+ with ([ga_mk (v2t ec) [] [garrowfy_code_types t] @@ nil]).
+ eapply nd_comp; [ apply arrange_esc | idtac ].
+ set (decide_tree_empty (take_lev (ec :: nil) succ)) as q'.
+ destruct q'.
+ destruct s.
+ rewrite e.
+ clear e.
+
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ].
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
+ eapply nd_comp; [ apply nd_llecnac | idtac ].
+ apply nd_prod; [ idtac | eapply boost ].
+ induction x.
+ apply ga_id.
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ].
+ apply ga_join.
+ apply IHx1.
+ apply IHx2.
+ unfold unlev'.
+ simpl.
+ apply postcompose.
+ apply ga_drop.
+
+ (* environment has non-empty leaves *)
+ apply (ga_kappa Γ Δ (v2t ec) nil (take_lev (ec::nil) succ) _ _).
+ apply (Prelude_error "found Esc at depth >0 (a)").
destruct case_RNote.
simpl.
destruct l; simpl.
apply nd_rule; apply RNote; auto.
- destruct (Peano_dec.eq_nat_dec (Datatypes.length l) n).
- apply nd_rule; apply RNote; auto.
apply nd_rule; apply RNote; auto.
destruct case_RLit.
destruct l0; simpl.
rewrite literal_types_unchanged.
apply nd_rule; apply RLit.
- destruct (Peano_dec.eq_nat_dec (Datatypes.length l0) n); unfold mapTree; unfold mapOptionTree; simpl.
unfold take_lev; simpl.
- unfold drop_depth; simpl.
- apply ga_lit.
+ unfold drop_lev; simpl.
+ unfold unlev'.
+ simpl.
rewrite literal_types_unchanged.
- apply nd_rule.
- apply RLit.
+ apply ga_lit.
destruct case_RVar.
Opaque flatten_judgment.
unfold getjlev.
destruct lev.
apply nd_rule. apply RVar.
- destruct (eqd_dec (Datatypes.length lev) n).
-
repeat drop_simplify.
+ unfold unlev'.
repeat take_simplify.
simpl.
apply ga_id.
- apply nd_rule.
- apply RVar.
-
destruct case_RGlobal.
simpl.
- destruct l as [|ec lev]; simpl; [ apply nd_rule; apply RGlobal; auto | idtac ].
- destruct (Peano_dec.eq_nat_dec (Datatypes.length lev) n); [ idtac | apply nd_rule; apply RGlobal; auto ]; simpl.
+ rename l into g.
+ rename σ into l.
+ destruct l as [|ec lev]; simpl; [ apply nd_rule; rewrite globals_do_not_have_code_types; apply RGlobal; auto | idtac ].
apply (Prelude_error "found RGlobal at depth >0").
destruct case_RLam.
- Opaque drop_depth.
+ Opaque drop_lev.
Opaque take_lev.
simpl.
destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RLam; auto | idtac ].
- destruct (Peano_dec.eq_nat_dec (Datatypes.length lev) n); [ idtac | apply nd_rule; apply RLam; auto ]; simpl.
- rewrite <- e.
- clear e n.
repeat drop_simplify.
repeat take_simplify.
eapply nd_comp.
apply RCanR.
apply boost.
apply ga_curry.
-
+
destruct case_RCast.
simpl.
destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RCast; auto | idtac ].
apply flatten_coercion; auto.
- destruct (Peano_dec.eq_nat_dec (Datatypes.length lev) n); [ idtac | apply nd_rule; apply RCast; auto ]; simpl.
apply (Prelude_error "RCast at level >0").
- apply flatten_coercion; auto.
destruct case_RJoin.
simpl.
simpl.
destruct lev as [|ec lev]. simpl. apply nd_rule.
- replace (garrowfy_code_types n (tx ---> te)) with ((garrowfy_code_types n tx) ---> (garrowfy_code_types n te)).
+ replace (garrowfy_code_types (tx ---> te)) with ((garrowfy_code_types tx) ---> (garrowfy_code_types te)).
apply RApp.
- unfold garrowfy_code_types.
- simpl.
reflexivity.
- destruct (Peano_dec.eq_nat_dec (Datatypes.length lev) n).
- eapply nd_comp.
- eapply nd_rule.
- apply RJoin.
- repeat drop_simplify.
+ repeat drop_simplify.
repeat take_simplify.
- apply boost.
- apply ga_apply.
-
- replace (garrowfy_code_types (minus' n (length (ec::lev))) (tx ---> te))
- with ((garrowfy_code_types (minus' n (length (ec::lev))) tx) --->
- (garrowfy_code_types (minus' n (length (ec::lev))) te)).
- apply nd_rule.
- apply RApp.
- unfold garrowfy_code_types.
- simpl.
+ rewrite mapOptionTree_distributes.
+ set (mapOptionTree (garrowfy_leveled_code_types ) (drop_lev (ec :: lev) Σ₁)) as Σ₁'.
+ set (mapOptionTree (garrowfy_leveled_code_types ) (drop_lev (ec :: lev) Σ₂)) as Σ₂'.
+ set (take_lev (ec :: lev) Σ₁) as Σ₁''.
+ set (take_lev (ec :: lev) Σ₂) as Σ₂''.
+ replace (garrowfy_code_types (tx ---> te)) with ((garrowfy_code_types tx) ---> (garrowfy_code_types te)).
+ apply (Prelude_error "FIXME: ga_apply").
reflexivity.
(*
Notation "` x" := (take_lev _ x) (at level 20).
Notation "`` x" := (mapOptionTree unlev x) (at level 20).
- Notation "``` x" := ((drop_depth _ x)) (at level 20).
+ Notation "``` x" := ((drop_lev _ x)) (at level 20).
Notation "!<[]> x" := (garrowfy_code_types _ x) (at level 1).
Notation "!<[@]>" := (garrowfy_leveled_code_types _) (at level 1).
*)
destruct case_RLet.
+ apply (Prelude_error "FIXME: RLet").
+(*
simpl.
destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RLet; auto | idtac ].
destruct (Peano_dec.eq_nat_dec (Datatypes.length lev) n); [ idtac | apply nd_rule; apply RLet; auto ]; simpl.
rename σ₂ into b.
rewrite mapOptionTree_distributes.
rewrite mapOptionTree_distributes.
- set (mapOptionTree (garrowfy_leveled_code_types (S n)) (drop_depth (ec :: lev) Σ₁)) as A.
+ set (mapOptionTree (garrowfy_leveled_code_types (S n)) (drop_lev (ec :: lev) Σ₁)) as A.
set (take_lev (ec :: lev) Σ₁) as A'.
- set (mapOptionTree (garrowfy_leveled_code_types (S n)) (drop_depth (ec :: lev) Σ₂)) as B.
+ set (mapOptionTree (garrowfy_leveled_code_types (S n)) (drop_lev (ec :: lev) Σ₂)) as B.
set (take_lev (ec :: lev) Σ₂) as B'.
simpl.
eapply RVar.
apply nd_id.
-
+*)
destruct case_RVoid.
simpl.
apply nd_rule.
apply RAppT.
apply Δ.
apply Δ.
- apply (Prelude_error "AppT at depth>0").
+ apply (Prelude_error "ga_apply").
destruct case_RAbsT.
simpl. destruct lev; simpl.
rewrite garrowfy_commutes_with_HaskTApp.
eapply nd_comp; [ idtac | eapply nd_rule; eapply RAbsT ].
simpl.
- set (mapOptionTree (garrowfy_leveled_code_types n) (mapOptionTree (weakLT(κ:=κ)) Σ)) as a.
- set (mapOptionTree (weakLT(κ:=κ)) (mapOptionTree (garrowfy_leveled_code_types n) Σ)) as q'.
+ set (mapOptionTree (garrowfy_leveled_code_types ) (mapOptionTree (weakLT(κ:=κ)) Σ)) as a.
+ set (mapOptionTree (weakLT(κ:=κ)) (mapOptionTree (garrowfy_leveled_code_types ) Σ)) as q'.
assert (a=q').
unfold a.
unfold q'.