| TCoerc _ t1 t2 t => TCoerc (flatten_rawtype t1) (flatten_rawtype t2) (flatten_rawtype t)
| TArrow => TArrow
| TCode ec e => let e' := flatten_rawtype e
- in ga_mk_raw ec (unleaves (take_arg_types e')) [drop_arg_types e']
+ in ga_mk_raw ec (unleaves_ (take_arg_types e')) [drop_arg_types e']
| TyFunApp tfc kl k lt => TyFunApp tfc kl k (flatten_rawtype_list _ lt)
end
with flatten_rawtype_list {TV}(lk:list Kind)(exp:@RawHaskTypeList TV lk) : @RawHaskTypeList TV lk :=
(mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) B))
(mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) A)) @@ nil]]
with
+ | RId a => let case_RId := tt in ga_id _ _ _ _ _
| RCanL a => let case_RCanL := tt in ga_uncancell _ _ _ _ _
| RCanR a => let case_RCanR := tt in ga_uncancelr _ _ _ _ _
| RuCanL a => let case_RuCanL := tt in ga_cancell _ _ _ _ _
match r as R in Arrange A B return
Arrange (mapOptionTree (flatten_leveled_type ) (drop_lev _ A))
(mapOptionTree (flatten_leveled_type ) (drop_lev _ B)) with
+ | RId a => let case_RId := tt in RId _
| RCanL a => let case_RCanL := tt in RCanL _
| RCanR a => let case_RCanR := tt in RCanR _
| RuCanL a => let case_RuCanL := tt in RuCanL _
apply nd_rule.
apply RArrange.
induction r; simpl.
+ apply RId.
apply RCanL.
apply RCanR.
apply RuCanL.
apply IHt2.
Defined.
- Axiom extensionality : forall Γ Q (f g:forall TV, InstantiatedTypeEnv TV Γ -> Q TV),
- (forall tv ite, f tv ite = g tv ite) -> f=g.
-
Lemma krunk : forall Γ (ec:HaskTyVar Γ ECKind) t,
flatten_type (<[ ec |- t ]>)
= @ga_mk Γ (v2t ec)
unfold flatten_type at 1.
simpl.
unfold ga_mk.
- apply extensionality.
+ apply phoas_extensionality.
intros.
unfold v2t.
unfold ga_mk_raw.
simpl.
replace (flatten_type (drop_arg_types_as_tree t) tv ite)
with (drop_arg_types (flatten_rawtype (t tv ite))).
- replace (unleaves (take_arg_types (flatten_rawtype (t tv ite))))
+ replace (unleaves_ (take_arg_types (flatten_rawtype (t tv ite))))
with ((mapOptionTree (fun x : HaskType Γ ★ => flatten_type x tv ite)
- (unleaves
+ (unleaves_
(take_trustme (count_arg_types (t (fun _ : Kind => unit) (ite_unit Γ)))
(fun TV : Kind → Type => take_arg_types ○ t TV))))).
reflexivity.
| 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.
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 RId.
+ 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 RCanR.
+ 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 RId.
+ 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 RuCanR.
+ 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).
simpl.
apply RLam.
simpl.
- rewrite take_works.
rewrite drop_works.
apply nd_rule.
apply SFlat.
apply RArrange.
+ eapply RComp.
apply RCossa.
+ apply RLeft.
+ apply take_arrange.
destruct case_RCast.
simpl.
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 ].
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.
+ apply nd_rule.
+ apply SFlat.
+ apply RArrange.
+ eapply RComp; [ idtac | eapply RAssoc ].
+ apply RLeft.
+ eapply RComp; [ idtac | apply RExch ].
+ apply take_unarrange.
destruct case_RLet.
simpl.