Skip to content

Instantly share code, notes, and snippets.

@mbrcknl
Created December 15, 2015 00:09
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save mbrcknl/9c0cffd051221a488d8a to your computer and use it in GitHub Desktop.
Save mbrcknl/9c0cffd051221a488d8a to your computer and use it in GitHub Desktop.
Require Import List.
Inductive type : Type :=
| base : type
| arr : type -> type -> type.
Infix "==>" := arr (right associativity, at level 52).
Inductive elem {A: Type} (x: A): list A -> Type :=
| here : forall xs, elem x (x :: xs)
| there : forall y xs, elem x xs -> elem x (y :: xs).
Arguments here {A x xs}.
Arguments there {A x y xs} _.
Fixpoint hlist {A: Type} (I: A -> Type) (is: list A): Type :=
match is with
| nil => unit
| cons j js => (I j * hlist I js) % type
end.
Fixpoint hat {A: Type} {I: A -> Type} {is} {x} (p: elem x is): hlist I is -> I x :=
match p with
| here _ => fun xs => fst xs
| there _ _ q => fun xs => hat q (snd xs)
end.
Module fo.
Inductive term (g : list type): type -> Type :=
| lam : forall s t, term (s::g) t -> term g (s ==> t)
| app : forall s t, term g (s ==> t) -> term g s -> term g t
| var : forall t, elem t g -> term g t.
Arguments lam {g s t} _.
Arguments app {g s t} _ _.
Arguments var {g t} _.
End fo.
Module ho.
Inductive term (v: type -> Type): type -> Type :=
| lam : forall s t, (v s -> term v t) -> term v (s ==> t)
| app : forall s t, term v (s ==> t) -> term v s -> term v t
| var : forall t, v t -> term v t.
Arguments lam {v s t} _.
Arguments app {v s t} _ _.
Arguments var {v t} _.
End ho.
Definition term t := forall v, ho.term v t.
Notation "[ t ]" := (fun _ => t).
Notation "^ v" :=
(ho.var v) (format "^ v", at level 49).
Notation "'lambda' x -> e" :=
(ho.lam (fun x => e)) (no associativity, at level 51, x at level 0).
Infix "@" :=
ho.app (left associativity, at level 50).
Definition twice t : term ((t ==> t) ==> (t ==> t)) :=
[ lambda f -> (lambda g -> lambda y -> ^f @ (^g @ ^y)) @ (lambda x -> ^f @ ^x) ].
Module wf.
Inductive wf (g: list type) (u v: type -> Type) (i: hlist u g) (j: hlist v g):
forall t, ho.term u t -> ho.term v t -> Prop :=
| lam :
forall s t (e: u s -> ho.term u t) (f: v s -> ho.term v t),
(forall x y, wf (s::g) u v (x,i) (y,j) t (e x) (f y)) ->
wf g u v i j (s ==> t) (lambda x -> e x) (lambda y -> f y)
| app :
forall s t
(f1: ho.term u (s ==> t))
(f2: ho.term v (s ==> t))
(a1: ho.term u s)
(a2: ho.term v s),
wf g u v i j (s ==> t) f1 f2 ->
wf g u v i j s a1 a2 ->
wf g u v i j t (f1 @ a1) (f2 @ a2)
| var :
forall t (p: elem t g) x y,
x = hat p i ->
y = hat p j ->
wf g u v i j t (^x) (^y).
End wf.
Definition wf {t} (e: term t) := forall u v, wf.wf nil u v tt tt t (e u) (e v).
Lemma hat_here:
forall A (I: A -> Type) i is (x: I i) (xs: hlist I is), x = hat here (x,xs).
Proof.
trivial.
Qed.
Lemma hat_there:
forall A (I: A -> Type) i j is (x: I i) (y: I j) (xs: hlist I is) (p: elem _ is),
x = hat p xs ->
x = hat (there p) (y,xs).
Proof.
trivial.
Qed.
Ltac show_wf :=
repeat econstructor;
repeat match goal with
| |- ?x = hat _ (?x,_) => eapply hat_here
| |- ?x = hat _ (?y,_) => eapply hat_there
end.
Theorem wf_twice: forall t, wf (twice t).
show_wf.
Qed.
Module equiv.
Inductive equiv (g: list type) (u: type -> Type) (i: hlist u g):
forall t, ho.term u t -> fo.term g t -> Prop :=
| lam :
forall s t (e: u s -> ho.term u t) y,
(forall x, equiv (s::g) u (x,i) t (e x) y) ->
equiv g u i (s ==> t) (lambda x -> e x) (fo.lam y)
| app :
forall s t (f: ho.term u (s ==> t)) (a: ho.term u s) e b,
equiv g u i (s ==> t) f e ->
equiv g u i s a b ->
equiv g u i t (f @ a) (fo.app e b)
| var :
forall t (p: elem t g) x,
x = hat p i ->
equiv g u i t (^x) (fo.var p).
End equiv.
Definition equiv {t} (e: term t) (f: fo.term nil t) :=
forall u, equiv.equiv nil u tt t (e u) f.
Definition lower_equiv {t} (e: term t) := { f | equiv e f }.
Definition twice_lower_equiv t: lower_equiv (twice t).
show_wf.
Defined.
Definition twice_lower t := proj1_sig (twice_lower_equiv t).
Fixpoint raise_impl {t g u} (f: fo.term g t) (e: hlist u g): ho.term u t :=
match f with
| fo.lam s r b => ho.lam (fun x => raise_impl b (x,e))
| fo.app s r k a => ho.app (raise_impl k e) (raise_impl a e)
| fo.var v p => ho.var (hat p e)
end.
Definition raise {t} (e: fo.term nil t): term t :=
fun _ => raise_impl e tt.
Definition twice_raised t := raise (twice_lower t).
Eval compute in twice_raised base.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment