Skip to content

Instantly share code, notes, and snippets.

@JasonGross

JasonGross/PHOAS_DTT.v

Last active October 2, 2017 04:22
Show Gist options
  • Save JasonGross/4142bce6a5aa4c9ebf99e30818e5ff68 to your computer and use it in GitHub Desktop.
Save JasonGross/4142bce6a5aa4c9ebf99e30818e5ff68 to your computer and use it in GitHub Desktop.
Download ZIP
PHOAS-like dependent types and terms in Coq
Raw
PHOAS_DTT.v
Inductive TYPE' : Type -> Type :=
| UNIT' : TYPE' unit
| EMPTY' : TYPE' Empty_set
| SIGMA' {a} (A : TYPE' a) {p} (P : forall v : a, TYPE' (p v)) : TYPE' (@sigT a p)
| PI' {a} (A : TYPE' a) {b} (B : forall v : a, TYPE' (b v)) : TYPE' (forall v : a, b v).
Definition TYPE := { T : _ & TYPE' T }.
Definition interp_TYPE : TYPE -> Type := @projT1 _ _.
Definition UNIT : TYPE := existT _ _ UNIT'.
Definition EMPTY : TYPE := existT _ _ EMPTY'.
Definition SIGMA (A : TYPE) (P : interp_TYPE A -> TYPE) : TYPE
:= existT _ _ (SIGMA' (projT2 A) (fun a => projT2 (P a))).
Definition PI (A : TYPE) (P : interp_TYPE A -> TYPE) : TYPE
:= existT _ _ (PI' (projT2 A) (fun a => projT2 (P a))).
Fixpoint TYPE_rect' (P : TYPE -> Type)
(u : P UNIT)
(e : P EMPTY)
(s : forall a (p : interp_TYPE a -> TYPE)
(a' : P a)
(p' : forall a', P (p a')),
P (SIGMA a p))
(pi : forall a (p : interp_TYPE a -> TYPE)
(a' : P a)
(p' : forall a', P (p a')),
P (PI a p))
t
(T : TYPE' t)
: P (existT _ t T)
:= match T in TYPE' t return P (existT _ t T) with
| UNIT' => u
| EMPTY' => e
| @SIGMA' a A p P'
=> s (existT _ _ A)
(fun a' => existT _ _ (P' a'))
(@TYPE_rect' P u e s pi _ _)
(fun _ => @TYPE_rect' P u e s pi _ _)
| @PI' a A b B
=> pi (existT _ _ A)
(fun a' => existT _ _ (B a'))
(@TYPE_rect' P u e s pi _ _)
(fun _ => @TYPE_rect' P u e s pi _ _)
end.
Definition TYPE_rect (P : TYPE -> Type)
(u : P UNIT)
(e : P EMPTY)
(s : forall a (p : interp_TYPE a -> TYPE)
(a' : P a)
(p' : forall a', P (p a')),
P (SIGMA a p))
(pi : forall a (p : interp_TYPE a -> TYPE)
(a' : P a)
(p' : forall a', P (p a')),
P (PI a p))
(T : TYPE)
: P T
:= match T with
| existT _ _ T => @TYPE_rect' P u e s pi _ T
end.
Inductive TERM' : forall T : TYPE, interp_TYPE T -> Type :=
| TT' : TERM' UNIT tt
| EXIST' {A : TYPE} (P : interp_TYPE A -> TYPE)
{a : interp_TYPE A} (x : @TERM' A a)
{b : interp_TYPE (P a)} (y : @TERM' (P a) b)
: TERM' (SIGMA A P) (existT _ a b)
| PROJ1' {A : TYPE} {P : interp_TYPE A -> TYPE}
{a : interp_TYPE (SIGMA A P)}
(v : @TERM' (SIGMA A P) a)
: TERM' A (projT1 a)
| PROJ2' {A : TYPE} {P : interp_TYPE A -> TYPE}
{a : interp_TYPE (SIGMA A P)}
(v : @TERM' (SIGMA A P) a)
: TERM' (P (projT1 a)) (projT2 a)
| LAMBDA' {A : TYPE} {B : interp_TYPE A -> TYPE}
{f : forall a, interp_TYPE (B a)} (F : forall a, @TERM' (B a) (f a))
: TERM' (PI A B) f
| APP' {A : TYPE} {B : interp_TYPE A -> TYPE}
{f : forall a, interp_TYPE (B a)} (F : @TERM' (PI A B) f)
{x : interp_TYPE A} (X : @TERM' A x)
: TERM' (B x) (f x).
Definition TERM (T : TYPE) : Type := { v : _ & @TERM' T v }.
Definition interp_TERM {T : TYPE} : TERM T -> interp_TYPE T := @projT1 _ _.
Definition TT : TERM UNIT := existT _ _ TT'.
Definition EXIST {A : TYPE} (P : interp_TYPE A -> TYPE)
(a : TERM A) (p : TERM (P (interp_TERM a)))
: TERM (SIGMA A P)
:= existT _ _ (EXIST' P (projT2 a) (projT2 p)).
Definition PROJ1 {A : TYPE} {P : interp_TYPE A -> TYPE}
(v : TERM (SIGMA A P))
: TERM A
:= existT _ _ (PROJ1' (projT2 v)).
Definition PROJ2 {A : TYPE} {P : interp_TYPE A -> TYPE}
(v : TERM (SIGMA A P))
: TERM (P (interp_TERM (PROJ1 v)))
:= existT _ _ (PROJ2' (projT2 v)).
Definition LAMBDA {A : TYPE} {B : interp_TYPE A -> TYPE}
(f : forall a, TERM (B a))
: TERM (PI A B)
:= existT _ _ (LAMBDA' (fun a => projT2 (f a))).
Definition APP {A : TYPE} {B : interp_TYPE A -> TYPE}
(f : TERM (PI A B))
(x : TERM A)
: TERM (B (interp_TERM x))
:= existT _ _ (APP' (projT2 f) (projT2 x)).
Fixpoint TERM_rect' (P : forall T : TYPE, TERM T -> Type)
(u : P UNIT TT)
(ex : forall (A : TYPE) (Q : interp_TYPE A -> TYPE)
(a : TERM A) (q : TERM (Q (interp_TERM a))),
P _ a -> P _ q -> P (SIGMA A Q) (EXIST Q a q))
(pr1 : forall (A : TYPE) (Q : interp_TYPE A -> TYPE)
(v : TERM (SIGMA A Q)),
P _ v -> P A (PROJ1 v))
(pr2 : forall (A : TYPE) (Q : interp_TYPE A -> TYPE)
(v : TERM (SIGMA A Q)) (pv : P _ v),
P _ (PROJ2 v))
(lam : forall (A : TYPE) (B : interp_TYPE A -> TYPE)
(f : forall a, TERM (B a)),
(forall a, P _ (f a)) -> P _ (LAMBDA f))
(app : forall (A : TYPE) (B : interp_TYPE A -> TYPE)
(f : TERM (PI A B))
(x : TERM A),
P _ f -> P _ x -> P _ (APP f x))
(T : TYPE)
(it : interp_TYPE T)
(t : @TERM' T it)
: P T (existT _ it t)
:= match t in @TERM' T it return P T (existT _ it t) with
| TT' => u
| @EXIST' A P' a x b y
=> ex A P' (existT _ a x) (existT _ b y)
(@TERM_rect' P u ex pr1 pr2 lam app _ _ _)
(@TERM_rect' P u ex pr1 pr2 lam app _ _ _)
| @PROJ1' A P' a v
=> pr1 A P' (existT _ a v)
(@TERM_rect' P u ex pr1 pr2 lam app _ _ _)
| @PROJ2' A P' a v
=> pr2 A P' (existT _ a v)
(@TERM_rect' P u ex pr1 pr2 lam app _ _ _)
| @LAMBDA' A B f F
=> lam A B (fun a => existT _ (f a) (F a))
(fun a => @TERM_rect' P u ex pr1 pr2 lam app _ _ _)
| @APP' A B f F x X
=> app A B (existT _ f F) (existT _ x X)
(@TERM_rect' P u ex pr1 pr2 lam app _ _ _)
(@TERM_rect' P u ex pr1 pr2 lam app _ _ _)
end.
Definition TERM_rect (P : forall T : TYPE, TERM T -> Type)
(u : P UNIT TT)
(ex : forall (A : TYPE) (Q : interp_TYPE A -> TYPE)
(a : TERM A) (q : TERM (Q (interp_TERM a))),
P _ a -> P _ q -> P (SIGMA A Q) (EXIST Q a q))
(pr1 : forall (A : TYPE) (Q : interp_TYPE A -> TYPE)
(v : TERM (SIGMA A Q)),
P _ v -> P A (PROJ1 v))
(pr2 : forall (A : TYPE) (Q : interp_TYPE A -> TYPE)
(v : TERM (SIGMA A Q)) (pv : P _ v),
P _ (PROJ2 v))
(lam : forall (A : TYPE) (B : interp_TYPE A -> TYPE)
(f : forall a, TERM (B a)),
(forall a, P _ (f a)) -> P _ (LAMBDA f))
(app : forall (A : TYPE) (B : interp_TYPE A -> TYPE)
(f : TERM (PI A B))
(x : TERM A),
P _ f -> P _ x -> P _ (APP f x))
(T : TYPE)
(t : TERM T)
: P T t
:= match t with
| existT _ _ t => @TERM_rect' P u ex pr1 pr2 lam app T _ t
end.
Raw
PHOAS_DTT_WITH_RECORDS.v
Set Primitive Projections.
Set Implicit Arguments.
Record sigT {A} (P : A -> Type) := existT { projT1 : A ; projT2 : P projT1 }.
Notation "{ x : A & P }" := (sigT (A:=A) (fun x => P)) : type_scope.
Add Printing Let sigT.
Arguments projT1 {A P} _.
Arguments projT2 {A P} _.
Arguments existT {A} P _ _.
Record prod A B := pair { fst : A ; snd : B }.
Arguments fst {A B} _.
Arguments snd {A B} _.
Arguments pair {A B} _ _.
Add Printing Let prod.
Notation "x * y" := (prod x y) : type_scope.
Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope.
Notation "( x ; y ; .. ; z )" := (existT _ .. (existT _ x y) .. z) : core_scope.
Inductive TYPE' : Type -> Type :=
| UNIT' : TYPE' unit
| EMPTY' : TYPE' Empty_set
| NAT' : TYPE' nat
| EQ' {a} {A : TYPE' a} (x y : a) : TYPE' (x = y)
| SIGMA' {a} (A : TYPE' a) {p} (P : forall v : a, TYPE' (p v)) : TYPE' (@sigT a p)
| PI' {a} (A : TYPE' a) {b} (B : forall v : a, TYPE' (b v)) : TYPE' (forall v : a, b v)
| RECORD' {s} (R : Type) (S : TYPE' s) (to_sigma : R -> s) (of_sigma : s -> R) : TYPE' R.
Arguments RECORD' {s} R S {to_sigma of_sigma}, {s} R S to_sigma of_sigma.
Definition TYPE := { T : _ & TYPE' T }.
Definition interp_TYPE : TYPE -> Type := @projT1 _ _.
Definition UNIT : TYPE := existT _ _ UNIT'.
Definition EMPTY : TYPE := existT _ _ EMPTY'.
Definition NAT : TYPE := existT _ _ NAT'.
Definition EQ {A : TYPE} (x y : interp_TYPE A) : TYPE
:= existT _ _ (@EQ' _ (projT2 A) x y).
Definition SIGMA (A : TYPE) (P : interp_TYPE A -> TYPE) : TYPE
:= existT _ _ (SIGMA' (projT2 A) (fun a => projT2 (P a))).
Definition PI (A : TYPE) (P : interp_TYPE A -> TYPE) : TYPE
:= existT _ _ (PI' (projT2 A) (fun a => projT2 (P a))).
Notation ARROW A B := (PI A (fun _ => B)).
Definition RECORD (R : Type) (S : TYPE) (to_sigma : R -> interp_TYPE S) (of_sigma : interp_TYPE S -> R) : TYPE
:= existT _ _ (@RECORD' _ R (projT2 S) to_sigma of_sigma).
Arguments RECORD R S {to_sigma of_sigma}, R S to_sigma of_sigma.
Fixpoint TYPE_rect' (P : TYPE -> Type)
(u : P UNIT)
(e : P EMPTY)
(n : P NAT)
(eq' : forall a (x y : interp_TYPE a), P a -> P (EQ x y))
(s : forall a (p : interp_TYPE a -> TYPE)
(a' : P a)
(p' : forall a', P (p a')),
P (SIGMA a p))
(pi : forall a (p : interp_TYPE a -> TYPE)
(a' : P a)
(p' : forall a', P (p a')),
P (PI a p))
(rec : forall R S (to_sigma : R -> interp_TYPE S) (of_sigma : interp_TYPE S -> R),
P S -> P (RECORD R S to_sigma of_sigma))
t
(T : TYPE' t)
: P (existT _ t T)
:= let TYPE_rect := @TYPE_rect' P u e n eq' s pi rec in
match T in TYPE' t return P (existT _ t T) with
| UNIT' => u
| EMPTY' => e
| NAT' => n
| @EQ' a A x y
=> eq' (existT _ _ A) x y
(TYPE_rect _ _)
| @SIGMA' a A p P'
=> s (existT _ _ A)
(fun a' => existT _ _ (P' a'))
(TYPE_rect _ _)
(fun _ => TYPE_rect _ _)
| @PI' a A b B
=> pi (existT _ _ A)
(fun a' => existT _ _ (B a'))
(TYPE_rect _ _)
(fun _ => TYPE_rect _ _)
| @RECORD' s R S' to_sigma of_sigma
=> rec R (existT _ _ S') to_sigma of_sigma
(TYPE_rect _ _)
end.
Definition TYPE_rect (P : TYPE -> Type)
(u : P UNIT)
(e : P EMPTY)
(n : P NAT)
(eq' : forall a (x y : interp_TYPE a), P a -> P (EQ x y))
(s : forall a (p : interp_TYPE a -> TYPE)
(a' : P a)
(p' : forall a', P (p a')),
P (SIGMA a p))
(pi : forall a (p : interp_TYPE a -> TYPE)
(a' : P a)
(p' : forall a', P (p a')),
P (PI a p))
(rec : forall R S (to_sigma : R -> interp_TYPE S) (of_sigma : interp_TYPE S -> R),
P S -> P (RECORD R S to_sigma of_sigma))
(T : TYPE)
: P T
:= match T with
| existT _ _ T => @TYPE_rect' P u e n eq' s pi rec _ T
end.
Inductive TERM' : forall T : TYPE, interp_TYPE T -> Type :=
| VAR' {T} (x : interp_TYPE T) : TERM' T x
| TT' : TERM' UNIT tt
| O' : TERM' NAT O
| S' : TERM' (ARROW NAT NAT) S
| NAT_RECT' (P : interp_TYPE NAT -> TYPE)
: TERM' (ARROW
(P O)
(ARROW
(PI NAT (fun n => ARROW (P n) (P (S n))))
(PI NAT P)))
(nat_rect (fun n => interp_TYPE (P n)))
| EQ_REFL' {A : TYPE}
: TERM' (PI A (fun x => @EQ A x x)) (@eq_refl (interp_TYPE A))
| EXIST' {A : TYPE} (P : interp_TYPE A -> TYPE)
{a : interp_TYPE A} (x : @TERM' A a)
{b : interp_TYPE (P a)} (y : @TERM' (P a) b)
: TERM' (SIGMA A P) (existT _ a b)
| PROJ1' {A : TYPE} {P : interp_TYPE A -> TYPE}
{a : interp_TYPE (SIGMA A P)}
(v : @TERM' (SIGMA A P) a)
: TERM' A (projT1 a)
| PROJ2' {A : TYPE} {P : interp_TYPE A -> TYPE}
{a : interp_TYPE (SIGMA A P)}
(v : @TERM' (SIGMA A P) a)
: TERM' (P (projT1 a)) (projT2 a)
| CONSTRUCT' {R : Type} {S : TYPE} {to_sigma of_sigma}
: TERM' (ARROW S (RECORD R S to_sigma of_sigma)) of_sigma
| PROJ_RECORD' {R : Type} {S : TYPE} {to_sigma of_sigma}
: TERM' (ARROW (RECORD R S to_sigma of_sigma) S) to_sigma
| LAMBDA' {A : TYPE} {B : interp_TYPE A -> TYPE}
{f : forall a, interp_TYPE (B a)}
(F : forall a, @TERM' (B a) (f a))
: TERM' (PI A B) f
| APP' {A : TYPE} {B : interp_TYPE A -> TYPE}
{f : forall a, interp_TYPE (B a)} (F : @TERM' (PI A B) f)
{x : interp_TYPE A} (X : @TERM' A x)
: TERM' (B x) (f x).
Definition TERM (T : TYPE) : Type := { v : _ & @TERM' T v }.
Definition interp_TERM {T : TYPE} : TERM T -> interp_TYPE T := @projT1 _ _.
Definition VAR {T} (x : interp_TYPE T) : TERM T := existT _ _ (VAR' x).
Definition TT : TERM UNIT := existT _ _ TT'.
Definition O : TERM NAT := existT _ _ O'.
Definition S : TERM (ARROW NAT NAT) := existT _ _ S'.
Definition NAT_RECT (P : interp_TYPE NAT -> TYPE)
: TERM (ARROW
(P 0)
(ARROW
(PI NAT (fun n => ARROW (P n) (P (Datatypes.S n))))
(PI NAT P)))
:= existT _ _ (NAT_RECT' P).
Definition EQ_REFL {A : TYPE}
: TERM (PI A (fun x => @EQ A x x))
:= existT _ _ (@EQ_REFL' A).
Arguments EQ_REFL {_}, _.
Definition EXIST {A : TYPE} (P : interp_TYPE A -> TYPE)
(a : TERM A) (p : TERM (P (interp_TERM a)))
: TERM (SIGMA A P)
:= existT _ _ (EXIST' P (projT2 a) (projT2 p)).
Definition PROJ1 {A : TYPE} {P : interp_TYPE A -> TYPE}
(v : TERM (SIGMA A P))
: TERM A
:= existT _ _ (PROJ1' (projT2 v)).
Definition PROJ2 {A : TYPE} {P : interp_TYPE A -> TYPE}
(v : TERM (SIGMA A P))
: TERM (P (interp_TERM (PROJ1 v)))
:= existT _ _ (PROJ2' (projT2 v)).
Definition CONSTRUCT {R : Type} {S : TYPE} {to_sigma of_sigma}
: TERM (ARROW S (RECORD R S to_sigma of_sigma))
:= existT _ _ CONSTRUCT'.
Definition PROJ_RECORD {R : Type} {S : TYPE} {to_sigma of_sigma}
: TERM (ARROW (RECORD R S to_sigma of_sigma) S)
:= existT _ _ PROJ_RECORD'.
Definition LAMBDA {A : TYPE} {B : interp_TYPE A -> TYPE}
(f : forall a, TERM (B a))
: TERM (PI A B)
:= existT _ _ (LAMBDA' (fun a => projT2 (f a))).
Definition APP {A : TYPE} {B : interp_TYPE A -> TYPE}
(f : TERM (PI A B))
(x : TERM A)
: TERM (B (interp_TERM x))
:= existT _ _ (APP' (projT2 f) (projT2 x)).
Fixpoint TERM_rect' (P : forall T : TYPE, TERM T -> Type)
(v : forall T x, P T (VAR x))
(u : P UNIT TT)
(o : P NAT O)
(s : P (ARROW NAT NAT) S)
(n_r : forall (Q : interp_TYPE NAT -> TYPE),
P _ (@NAT_RECT Q))
(eq_r : forall A, P _ (@EQ_REFL A))
(ex : forall (A : TYPE) (Q : interp_TYPE A -> TYPE)
(a : TERM A) (q : TERM (Q (interp_TERM a))),
P _ a -> P _ q -> P (SIGMA A Q) (EXIST Q a q))
(pr1 : forall (A : TYPE) (Q : interp_TYPE A -> TYPE)
(v : TERM (SIGMA A Q)),
P _ v -> P A (PROJ1 v))
(pr2 : forall (A : TYPE) (Q : interp_TYPE A -> TYPE)
(v : TERM (SIGMA A Q)) (pv : P _ v),
P _ (PROJ2 v))
(construct
: forall (R : Type) (S : TYPE) to_sigma of_sigma,
P _ (@CONSTRUCT R S to_sigma of_sigma))
(proj_record
: forall (R : Type) (S : TYPE) to_sigma of_sigma,
P _ (@PROJ_RECORD R S to_sigma of_sigma))
(lam : forall (A : TYPE) (B : interp_TYPE A -> TYPE)
(f : forall a, TERM (B a)),
(forall a, P _ (f a)) -> P _ (LAMBDA f))
(app : forall (A : TYPE) (B : interp_TYPE A -> TYPE)
(f : TERM (PI A B))
(x : TERM A),
P _ f -> P _ x -> P _ (APP f x))
(T : TYPE)
(it : interp_TYPE T)
(t : @TERM' T it)
: P T (existT _ it t)
:= let TERM_rect := TERM_rect' P v u o s n_r eq_r ex pr1 pr2 construct proj_record lam app in
match t in @TERM' T it return P T (existT _ it t) with
| @VAR' T x => v T x
| TT' => u
| O' => o
| S' => s
| @NAT_RECT' P' => n_r P'
| @EQ_REFL' A => eq_r A
| @EXIST' A P' a x b y
=> ex A P' (existT _ a x) (existT _ b y)
(TERM_rect _ _ _)
(TERM_rect _ _ _)
| @PROJ1' A P' a v
=> pr1 A P' (existT _ a v)
(TERM_rect _ _ _)
| @PROJ2' A P' a v
=> pr2 A P' (existT _ a v)
(TERM_rect _ _ _)
| @CONSTRUCT' R S'' to_sigma of_sigma
=> construct R S'' to_sigma of_sigma
| @PROJ_RECORD' R S'' to_sigma of_sigma
=> proj_record R S'' to_sigma of_sigma
| @LAMBDA' A B f F
=> lam A B (fun a => existT _ (f a) (F a))
(fun a => TERM_rect _ _ _)
| @APP' A B f F x X
=> app A B (existT _ f F) (existT _ x X)
(TERM_rect _ _ _)
(TERM_rect _ _ _)
end.
Definition TERM_rect (P : forall T : TYPE, TERM T -> Type)
(v : forall T x, P T (VAR x))
(u : P UNIT TT)
(o : P NAT O)
(s : P (ARROW NAT NAT) S)
(n_r : forall (Q : interp_TYPE NAT -> TYPE),
P _ (@NAT_RECT Q))
(eq_r : forall A, P _ (@EQ_REFL A))
(ex : forall (A : TYPE) (Q : interp_TYPE A -> TYPE)
(a : TERM A) (q : TERM (Q (interp_TERM a))),
P _ a -> P _ q -> P (SIGMA A Q) (EXIST Q a q))
(pr1 : forall (A : TYPE) (Q : interp_TYPE A -> TYPE)
(v : TERM (SIGMA A Q)),
P _ v -> P A (PROJ1 v))
(pr2 : forall (A : TYPE) (Q : interp_TYPE A -> TYPE)
(v : TERM (SIGMA A Q)) (pv : P _ v),
P _ (PROJ2 v))
(construct
: forall (R : Type) (S : TYPE) to_sigma of_sigma,
P _ (@CONSTRUCT R S to_sigma of_sigma))
(proj_record
: forall (R : Type) (S : TYPE) to_sigma of_sigma,
P _ (@PROJ_RECORD R S to_sigma of_sigma))
(lam : forall (A : TYPE) (B : interp_TYPE A -> TYPE)
(f : forall a, TERM (B a)),
(forall a, P _ (f a)) -> P _ (LAMBDA f))
(app : forall (A : TYPE) (B : interp_TYPE A -> TYPE)
(f : TERM (PI A B))
(x : TERM A),
P _ f -> P _ x -> P _ (APP f x))
(T : TYPE)
(t : TERM T)
: P T t
:= match t with
| existT _ _ t => @TERM_rect' P v u o s n_r eq_r ex pr1 pr2 construct proj_record lam app T _ t
end.
Ltac strip_args T ctor :=
lazymatch type of ctor with
| context[T]
=> match eval cbv beta in ctor with
| ?ctor _ => strip_args T ctor
| _ => ctor
end
end.
Ltac get_ctor T :=
let full_ctor := constr:(ltac:(let x := fresh in intro x; econstructor; apply x) : T -> T) in
let ctor := constr:(fun x : T => ltac:(let v := strip_args T (full_ctor x) in exact v)) in
lazymatch ctor with
| fun _ => ?ctor => ctor
end.
Ltac uncurry_domain f :=
lazymatch type of f with
| forall (a : ?A) (b : @?B a), _
=> uncurry_domain (fun ab : { a : A & B a } => f (projT1 ab) (projT2 ab))
| _ => eval cbv beta in f
end.
Ltac get_of_sigma T :=
let ctor := get_ctor T in
uncurry_domain ctor.
Ltac repeat_existT :=
lazymatch goal with
| [ |- sigT _ ] => simple refine (existT _ _ _); [ repeat_existT | shelve ]
| _ => shelve
end.
Ltac prove_to_of_sigma_goal of_sigma :=
let v := fresh "v" in
try unfold of_sigma;
simple refine (exist _ _ (fun v => _));
[ intro v; destruct v; repeat_existT
| let temp := fresh in
lazymatch goal with
| [ |- id ?k ?v = ?v' ]
=> pose k as temp;
change (id temp v = v')
end;
cbv beta;
repeat match goal with
| [ |- context[projT2 ?k] ]
=> let x := fresh "x" in
is_var k;
destruct k as [k x]; cbn [projT1 projT2]
end;
unfold id; cbv delta [temp]; reflexivity ].
Ltac prove_to_of_sigma of_sigma :=
constr:(
ltac:(prove_to_of_sigma_goal of_sigma)
: { to_sigma : _ | forall v, id to_sigma (of_sigma v) = v }).
Ltac get_to_sigma_gen of_sigma :=
let v := prove_to_of_sigma of_sigma in
eval hnf in (proj1_sig v).
Ltac get_to_sigma T :=
let of_sigma := get_of_sigma T in
get_to_sigma_gen of_sigma.
Ltac as_0arg_record R :=
constr:(RECORD
R
UNIT
(fun v => let () := v in tt)
(fun v => let '(tt) := v in (ltac:(constructor) : R))).
Ltac pre_as_narg_record R :=
let of_sigma := get_of_sigma R in
let to_sigma := get_to_sigma_gen of_sigma in
let t := type of of_sigma in
constr:(fun S
=> RECORD
R
(existT _ _ S)
to_sigma
of_sigma).
Ltac as_narg_record reify_TYPE R :=
let of_sigma := get_of_sigma R in
let to_sigma := get_to_sigma_gen of_sigma in
let s := lazymatch type of of_sigma with ?S -> _ => S end in
let S := reify_TYPE s in
constr:(RECORD
R
S
to_sigma
of_sigma).
Ltac reify_TYPE T :=
(*let dummy := match goal with _ => let T := eval hnf in T in idtac T end in*)
lazymatch (eval hnf in T) with
| unit => UNIT
| Empty_set => EMPTY
| nat => NAT
| @eq ?a ?x ?y
=> let A := reify_TYPE a in
constr:(@EQ A x y)
| @sigT ?a ?p
=> let A := reify_TYPE a in
let P := constr:(fun v : a => ltac:(let k := reify_TYPE (p v) in exact k)) in
constr:(@SIGMA A P)
| forall x : ?a, @?b x
=> let A := reify_TYPE a in
constr:(PI A (fun x : a => ltac:(let k := reify_TYPE (b x) in exact k)))
| ?R
=> match goal with
| _ => as_0arg_record R
| _ => as_narg_record reify_TYPE R
| _ => fail 1 "Failed to reify" R
end
end.
Definition reify_var {T rT} (v : T) (v' : rT) := True.
Ltac head term :=
lazymatch term with
| ?f _ => head f
| ?term => term
end.
Definition record_to_sigma_mark {T} (x : T) : T := x.
Ltac reify_TERM term :=
(*let dummy := match goal with _ => idtac term end in*)
lazymatch goal with
| [ H : reify_var term ?rTerm |- _ ] => rTerm
| _
=> lazymatch term with
| tt => TT
| Datatypes.O => O
| Datatypes.S => S
| @Datatypes.nat_rect ?p
=> let P := constr:(fun n : nat => ltac:(let v := reify_TYPE (p n) in exact v)) in
constr:(@NAT_RECT P)
| @eq_refl ?a
=> let A :=reify_TYPE a in
constr:(@EQ_REFL A)
| projT1 ?v
=> let V := reify_TERM v in
constr:(PROJ1 V)
| projT2 ?v
=> let V := reify_TERM v in
constr:(PROJ2 V)
| @existT ?a ?p ?x ?y
=> let A := reify_TYPE a in
let P := constr:(fun aa : a => ltac:(let v := reify_TYPE (p aa) in exact v)) in
let X := reify_TERM x in
let Y := reify_TERM y in
constr:(@EXIST A P X Y)
| (fun x : ?a => ?p)
=> let A := reify_TYPE a in
let maybe_x := fresh x in
let probably_not_x := fresh maybe_x in
let not_x := fresh probably_not_x in
let rx := fresh not_x in
let lam := constr:(fun (x : a) (_ : reify_var x (@VAR A x))
=> match p with
| not_x
=> ltac:(let v := (eval cbv delta [not_x] in not_x) in
let v := reify_TERM v in
exact v)
end) in
lazymatch lam with
| fun x _ => @?lam x => constr:(@LAMBDA A _ lam)
end
| record_to_sigma_mark _ ?v
=> let V := reify_TERM v in
constr:(APP PROJ_RECORD V)
| ?term
=> let t := type of term in
let T := reify_TYPE t in
let is_record_ctor
:= match T with
| RECORD _ _ _ _
=> let h := head term in
let success := match goal with
| _ => is_constructor h
end in
true
| _ => false
end in
lazymatch is_record_ctor with
| true
=> lazymatch T with
| RECORD ?R ?S ?to_sigma ?of_sigma
=> let term := (eval cbv beta iota in (to_sigma term)) in
let term' := reify_TERM term in
constr:(APP (@CONSTRUCT R S to_sigma of_sigma) term')
end
| false
=> lazymatch term with
| ?f ?x
=> let F := reify_TERM f in
let X := reify_TERM x in
constr:(APP F X)
end
end
end
end.
Ltac codomain T :=
lazymatch T with
| _ -> ?T => codomain T
| forall x : ?A, ?P
=> let not_x := fresh x in
let not_x := fresh not_x in
let not_x := fresh not_x in
lazymatch constr:(forall x : A,
match P with
| not_x => ltac:(let v := (eval cbv delta [not_x] in not_x) in
let v := codomain v in
exact v)
end) with
| _ -> ?T => T
| ?T => T
end
| ?T => T
end.
Ltac change_with_in from to term :=
let v := constr:(ltac:(let k := fresh in
pose term as k;
change from with to in k;
let k' := (eval cbv delta [k] in k) in
exact k')) in
lazymatch v with
| let _ := _ in ?v => eval cbv beta in v
end.
Ltac mark_projections_in under_family_with_proj proj term :=
let new_proj
:= under_family_with_proj
ltac:(fun proj'
=> let t := type of proj' in
let t := lazymatch t with
| forall x : ?R, _ => R
end in
let T := pre_as_narg_record t in
lazymatch T with
| fun _ => @RECORD _ _ ?to_sigma ?of_sigma
=> let proj'' := (eval compute in proj') in
let v :=
(eval cbv beta iota in
(fun v => proj'' (of_sigma (record_to_sigma_mark to_sigma v)))) in
exact v
end) in
change_with_in proj new_proj term.
Ltac mark_0param_proj proj term :=
mark_projections_in
ltac:(fun tac => tac proj)
proj term.
Ltac mark_1param_proj proj term :=
mark_projections_in
ltac:(fun tac => constr:(fun A => ltac:(tac (proj A))))
proj term.
Ltac mark_2param_proj proj term :=
mark_projections_in
ltac:(fun tac => constr:(fun A B => ltac:(tac (proj A B))))
proj term.
Ltac mark_known_projections term :=
let term := mark_2param_proj (@fst) term in
let term := mark_2param_proj (@snd) term in
term.
Goal True.
let k := reify_TYPE (unit * unit)%type in pose k.
let k := reify_TERM (tt, tt) in pose k; cbv beta in *.
let term := constr:(fst (tt, tt)) in
let term := mark_known_projections term in
let k := reify_TERM term in pose k; cbv beta in *.
let term := constr:(eq_refl (nat_rect (fun _ => nat) 0 (fun n _ => n))) in
let term := mark_known_projections term in
let k := reify_TERM term in pose k; cbv beta in *.
Abort.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment