Library MetaCoq.Translations.param_original
Infix "≤" := Nat.leb.
Definition default_term := tVar "constant_not_found".
Definition debug_term msg:= tVar ("debug: " ++ msg).
Fixpoint tsl_rec0 (n : nat) (t : term) {struct t} : term :=
match t with
| tRel k ⇒ if n ≤ k then tRel (2×k-n+1) else t
| tEvar k ts ⇒ tEvar k (map (tsl_rec0 n) ts)
| tCast t c a ⇒ tCast (tsl_rec0 n t) c (tsl_rec0 n a)
| tProd na A B ⇒ tProd na (tsl_rec0 n A) (tsl_rec0 (n+1) B)
| tLambda na A t ⇒ tLambda na (tsl_rec0 n A) (tsl_rec0 (n+1) t)
| tLetIn na t A u ⇒ tLetIn na (tsl_rec0 n t) (tsl_rec0 n A) (tsl_rec0 (n+1) u)
| tApp t lu ⇒ tApp (tsl_rec0 n t) (map (tsl_rec0 n) lu)
| tCase ik t u br ⇒ tCase ik (tsl_rec0 n t) (tsl_rec0 n u)
(map (fun x ⇒ (fst x, tsl_rec0 n (snd x))) br)
| tProj p t ⇒ tProj p (tsl_rec0 n t)
| _ ⇒ t
end.
Fixpoint subst_app (t : term) (us : list term) : term :=
match t, us with
| tLambda _ A t, u :: us ⇒ subst_app (t {0 := u}) us
| _, [] ⇒ t
| _, _ ⇒ mkApps t us
end.
Fixpoint tsl_rec1_app (app : option term) (E : tsl_table) (t : term) : term :=
let tsl_rec1 := tsl_rec1_app None in
let debug case symbol :=
debug_term ("tsl_rec1: " ++ case ++ " " ++ symbol ++ " not found") in
match t with
| tLambda na A t ⇒
let A0 := tsl_rec0 0 A in
let A1 := tsl_rec1_app None E A in
tLambda na A0 (tLambda (tsl_name tsl_ident na)
(subst_app (lift0 1 A1) [tRel 0])
(tsl_rec1_app (option_map (lift 2 2) app) E t))
| t ⇒ let t1 :=
match t with
| tRel k ⇒ tRel (2 × k)
| tSort s ⇒ tLambda (nNamed "A") (tSort s) (tProd nAnon (tRel 0) (tSort s))
| tProd na A B ⇒
let A0 := tsl_rec0 0 A in
let A1 := tsl_rec1 E A in
let B0 := tsl_rec0 1 B in
let B1 := tsl_rec1 E B in
let ΠAB0 := tProd na A0 B0 in
tLambda (nNamed "f") ΠAB0
(tProd na (lift0 1 A0)
(tProd (tsl_name tsl_ident na)
(subst_app (lift0 2 A1) [tRel 0])
(subst_app (lift 1 2 B1)
[tApp (tRel 2) [tRel 1]])))
| tApp t us ⇒
let us' := concat (map (fun v ⇒ [tsl_rec0 0 v; tsl_rec1 E v]) us) in
mkApps (tsl_rec1 E t) us'
| tLetIn na t A u ⇒
let t0 := tsl_rec0 0 t in
let t1 := tsl_rec1 E t in
let A0 := tsl_rec0 0 A in
let A1 := tsl_rec1 E A in
let u0 := tsl_rec0 0 u in
let u1 := tsl_rec1 E u in
tLetIn na t0 A0 (tLetIn (tsl_name tsl_ident na) (lift0 1 t1)
(subst_app (lift0 1 A1) [tRel 0]) u1)
| tCast t c A ⇒ let t0 := tsl_rec0 0 t in
let t1 := tsl_rec1 E t in
let A0 := tsl_rec0 0 A in
let A1 := tsl_rec1 E A in
tCast t1 c (mkApps A1 [tCast t0 c A0])
| tConst s univs ⇒
match lookup_tsl_table E (ConstRef s) with
| Some t ⇒ t
| None ⇒ debug "tConst" s
end
| tInd i univs ⇒
match lookup_tsl_table E (IndRef i) with
| Some t ⇒ t
| None ⇒ debug "tInd" (match i with mkInd s _ ⇒ s end)
end
| tConstruct i n univs ⇒
match lookup_tsl_table E (ConstructRef i n) with
| Some t ⇒ t
| None ⇒ debug "tConstruct" (match i with mkInd s _ ⇒ s end)
end
| tCase ik t u brs as case ⇒
let brs' := List.map (on_snd (lift0 1)) brs in
let case1 := tCase ik (lift0 1 t) (tRel 0) brs' in
match lookup_tsl_table E (IndRef (fst ik)) with
| Some (tInd i _univ) ⇒
tCase (i, (snd ik) × 2)
(tsl_rec1_app (Some (tsl_rec0 0 case1)) E t)
(tsl_rec1 E u)
(map (on_snd (tsl_rec1 E)) brs)
| _ ⇒ debug "tCase" (match (fst ik) with mkInd s _ ⇒ s end)
end
| tProj _ _ ⇒ todo
| tFix _ _ | tCoFix _ _ ⇒ todo
| tVar _ | tEvar _ _ ⇒ todo
| tLambda _ _ _ ⇒ tVar "impossible"
end in
match app with Some t' ⇒ mkApp t1 (t' {3 := tRel 1} {2 := tRel 0})
| None ⇒ t1 end
end.
Definition tsl_rec1 := tsl_rec1_app None.
Definition tsl_mind_body (E : tsl_table) (mp : string) (kn : kername)
(mind : mutual_inductive_body) : tsl_table × list mutual_inductive_body.
Defined.
Instance param : Translation :=
{| tsl_id := tsl_ident ;
tsl_tm := fun ΣE t ⇒ ret (tsl_rec1 (snd ΣE) t) ;
tsl_ty := None ;
tsl_ind := fun ΣE mp kn mind ⇒ ret (tsl_mind_body (snd ΣE) mp kn mind) |}.
Definition T := ∀ A, A → A.
Definition tm := ((fun A (x:A) ⇒ x) (Type → Type) (fun x ⇒ x)).
Module Id1.
Definition ID := ∀ A, A → A.
Lemma param_ID_identity (f : ID)
: IDᵗ f → ∀ A x, f A x = x.
Definition toto := fun n : nat ⇒ (fun y ⇒ 0) (fun _ : Type ⇒ n).
Definition my_id : ID :=
let n := 12 in (fun (_ : nat) y ⇒ y) 4 (fun A x ⇒ (fun _ : nat ⇒ x) n).
Definition free_thm_my_id : ∀ A x, my_id A x = x
:= param_ID_identity my_id my_idᵗ.
End Id1.
Module Id2.
Definition ID := ∀ A x y (p : x = y :> A), x = y.
Lemma param_ID_identity (f : ID)
: IDᵗ f → ∀ A x y p, f A x y p = p.
Definition myf : ID
:= fun A x y p ⇒ eq_trans (eq_trans p (eq_sym p)) p.
Definition free_thm_myf : ∀ A x y p, myf A x y p = p
:= param_ID_identity myf myfᵗ.
End Id2.
Module Vectors.
End Vectors.
Definition rev_type := ∀ A, list A → list A.
Module Axioms.
Definition UIP := ∀ A (x y : A) (p q : x = y), p = q.
Definition eqᵗ_eq {A Aᵗ x xᵗ y yᵗ p}
: eqᵗ A Aᵗ x xᵗ y yᵗ p → p # xᵗ = yᵗ.
Definition eq_eqᵗ {A Aᵗ x xᵗ y yᵗ p}
: p # xᵗ = yᵗ → eqᵗ A Aᵗ x xᵗ y yᵗ p.
Definition eqᵗ_eq_equiv A Aᵗ x xᵗ y yᵗ p
: eqᵗ A Aᵗ x xᵗ y yᵗ p <~> p # xᵗ = yᵗ.
Theorem UIP_provably_parametric : ∀ h : UIP, UIPᵗ h.
Definition wFunext
:= ∀ A (B : A → Type) (f g : ∀ x, B x), (∀ x, f x = g x) → f = g.
Theorem wFunext_provably_parametric : ∀ h : wFunext, wFunextᵗ h.
Definition wUnivalence := ∀ A B, A <~> B → A = B.
Theorem wUnivalence_provably_parametric : ∀ h, wUnivalenceᵗ h.
Definition equiv_paths {A B} (p : A = B) : A <~> B
:= transport (Equiv A) p equiv_idmap.
Definition Univalence := ∀ A B (p : A = B), IsEquiv (equiv_paths p).
Definition coe {A B} (p : A = B) : A → B := transport idmap p.
Definition Univalence' := ∀ A B (p : A = B), IsEquiv (coe p).
Definition UU' : Univalence' → Univalence.
Defined.
Lemma pathsᵗ_ok {A} {Aᵗ : A → Type} {x y} {xᵗ : Aᵗ y} (p : x = y)
: pathsᵗ A Aᵗ x (transport Aᵗ p^ xᵗ) y xᵗ p.
Lemma pathsᵗ_ok2 {A} {Aᵗ : A → Type} {x y} {xᵗ : Aᵗ y} (p q : x = y) e r
(Hr : e # (pathsᵗ_ok p) = r)
: pathsᵗ (x = y) (pathsᵗ A Aᵗ x (transport Aᵗ p^ xᵗ) y xᵗ) p (pathsᵗ_ok p) q r e.
Definition apᵗ_idmap {A} {Aᵗ : A → Type} {x y xᵗ yᵗ} (p : x = y)
(pᵗ : pathsᵗ A Aᵗ x xᵗ y yᵗ p)
: apᵗ A Aᵗ A Aᵗ idmap (fun u ⇒ idmap) x xᵗ y yᵗ p pᵗ = (ap_idmap p)^ # pᵗ.
Definition U'U : Univalence → Univalence'.
Defined.
Theorem Univalence'_provably_parametric : ∀ h : Univalence', Univalence'ᵗ h.
Definition Univalence_wFunext : Univalence → wFunext.
Admitted.
Theorem Univalence_provably_parametric : ∀ h : Univalence, Univalenceᵗ h.
End Axioms.
Definition default_term := tVar "constant_not_found".
Definition debug_term msg:= tVar ("debug: " ++ msg).
Fixpoint tsl_rec0 (n : nat) (t : term) {struct t} : term :=
match t with
| tRel k ⇒ if n ≤ k then tRel (2×k-n+1) else t
| tEvar k ts ⇒ tEvar k (map (tsl_rec0 n) ts)
| tCast t c a ⇒ tCast (tsl_rec0 n t) c (tsl_rec0 n a)
| tProd na A B ⇒ tProd na (tsl_rec0 n A) (tsl_rec0 (n+1) B)
| tLambda na A t ⇒ tLambda na (tsl_rec0 n A) (tsl_rec0 (n+1) t)
| tLetIn na t A u ⇒ tLetIn na (tsl_rec0 n t) (tsl_rec0 n A) (tsl_rec0 (n+1) u)
| tApp t lu ⇒ tApp (tsl_rec0 n t) (map (tsl_rec0 n) lu)
| tCase ik t u br ⇒ tCase ik (tsl_rec0 n t) (tsl_rec0 n u)
(map (fun x ⇒ (fst x, tsl_rec0 n (snd x))) br)
| tProj p t ⇒ tProj p (tsl_rec0 n t)
| _ ⇒ t
end.
Fixpoint subst_app (t : term) (us : list term) : term :=
match t, us with
| tLambda _ A t, u :: us ⇒ subst_app (t {0 := u}) us
| _, [] ⇒ t
| _, _ ⇒ mkApps t us
end.
Fixpoint tsl_rec1_app (app : option term) (E : tsl_table) (t : term) : term :=
let tsl_rec1 := tsl_rec1_app None in
let debug case symbol :=
debug_term ("tsl_rec1: " ++ case ++ " " ++ symbol ++ " not found") in
match t with
| tLambda na A t ⇒
let A0 := tsl_rec0 0 A in
let A1 := tsl_rec1_app None E A in
tLambda na A0 (tLambda (tsl_name tsl_ident na)
(subst_app (lift0 1 A1) [tRel 0])
(tsl_rec1_app (option_map (lift 2 2) app) E t))
| t ⇒ let t1 :=
match t with
| tRel k ⇒ tRel (2 × k)
| tSort s ⇒ tLambda (nNamed "A") (tSort s) (tProd nAnon (tRel 0) (tSort s))
| tProd na A B ⇒
let A0 := tsl_rec0 0 A in
let A1 := tsl_rec1 E A in
let B0 := tsl_rec0 1 B in
let B1 := tsl_rec1 E B in
let ΠAB0 := tProd na A0 B0 in
tLambda (nNamed "f") ΠAB0
(tProd na (lift0 1 A0)
(tProd (tsl_name tsl_ident na)
(subst_app (lift0 2 A1) [tRel 0])
(subst_app (lift 1 2 B1)
[tApp (tRel 2) [tRel 1]])))
| tApp t us ⇒
let us' := concat (map (fun v ⇒ [tsl_rec0 0 v; tsl_rec1 E v]) us) in
mkApps (tsl_rec1 E t) us'
| tLetIn na t A u ⇒
let t0 := tsl_rec0 0 t in
let t1 := tsl_rec1 E t in
let A0 := tsl_rec0 0 A in
let A1 := tsl_rec1 E A in
let u0 := tsl_rec0 0 u in
let u1 := tsl_rec1 E u in
tLetIn na t0 A0 (tLetIn (tsl_name tsl_ident na) (lift0 1 t1)
(subst_app (lift0 1 A1) [tRel 0]) u1)
| tCast t c A ⇒ let t0 := tsl_rec0 0 t in
let t1 := tsl_rec1 E t in
let A0 := tsl_rec0 0 A in
let A1 := tsl_rec1 E A in
tCast t1 c (mkApps A1 [tCast t0 c A0])
| tConst s univs ⇒
match lookup_tsl_table E (ConstRef s) with
| Some t ⇒ t
| None ⇒ debug "tConst" s
end
| tInd i univs ⇒
match lookup_tsl_table E (IndRef i) with
| Some t ⇒ t
| None ⇒ debug "tInd" (match i with mkInd s _ ⇒ s end)
end
| tConstruct i n univs ⇒
match lookup_tsl_table E (ConstructRef i n) with
| Some t ⇒ t
| None ⇒ debug "tConstruct" (match i with mkInd s _ ⇒ s end)
end
| tCase ik t u brs as case ⇒
let brs' := List.map (on_snd (lift0 1)) brs in
let case1 := tCase ik (lift0 1 t) (tRel 0) brs' in
match lookup_tsl_table E (IndRef (fst ik)) with
| Some (tInd i _univ) ⇒
tCase (i, (snd ik) × 2)
(tsl_rec1_app (Some (tsl_rec0 0 case1)) E t)
(tsl_rec1 E u)
(map (on_snd (tsl_rec1 E)) brs)
| _ ⇒ debug "tCase" (match (fst ik) with mkInd s _ ⇒ s end)
end
| tProj _ _ ⇒ todo
| tFix _ _ | tCoFix _ _ ⇒ todo
| tVar _ | tEvar _ _ ⇒ todo
| tLambda _ _ _ ⇒ tVar "impossible"
end in
match app with Some t' ⇒ mkApp t1 (t' {3 := tRel 1} {2 := tRel 0})
| None ⇒ t1 end
end.
Definition tsl_rec1 := tsl_rec1_app None.
Definition tsl_mind_body (E : tsl_table) (mp : string) (kn : kername)
(mind : mutual_inductive_body) : tsl_table × list mutual_inductive_body.
Defined.
Instance param : Translation :=
{| tsl_id := tsl_ident ;
tsl_tm := fun ΣE t ⇒ ret (tsl_rec1 (snd ΣE) t) ;
tsl_ty := None ;
tsl_ind := fun ΣE mp kn mind ⇒ ret (tsl_mind_body (snd ΣE) mp kn mind) |}.
Definition T := ∀ A, A → A.
Definition tm := ((fun A (x:A) ⇒ x) (Type → Type) (fun x ⇒ x)).
Module Id1.
Definition ID := ∀ A, A → A.
Lemma param_ID_identity (f : ID)
: IDᵗ f → ∀ A x, f A x = x.
Definition toto := fun n : nat ⇒ (fun y ⇒ 0) (fun _ : Type ⇒ n).
Definition my_id : ID :=
let n := 12 in (fun (_ : nat) y ⇒ y) 4 (fun A x ⇒ (fun _ : nat ⇒ x) n).
Definition free_thm_my_id : ∀ A x, my_id A x = x
:= param_ID_identity my_id my_idᵗ.
End Id1.
Module Id2.
Definition ID := ∀ A x y (p : x = y :> A), x = y.
Lemma param_ID_identity (f : ID)
: IDᵗ f → ∀ A x y p, f A x y p = p.
Definition myf : ID
:= fun A x y p ⇒ eq_trans (eq_trans p (eq_sym p)) p.
Definition free_thm_myf : ∀ A x y p, myf A x y p = p
:= param_ID_identity myf myfᵗ.
End Id2.
Module Vectors.
End Vectors.
Definition rev_type := ∀ A, list A → list A.
Module Axioms.
Definition UIP := ∀ A (x y : A) (p q : x = y), p = q.
Definition eqᵗ_eq {A Aᵗ x xᵗ y yᵗ p}
: eqᵗ A Aᵗ x xᵗ y yᵗ p → p # xᵗ = yᵗ.
Definition eq_eqᵗ {A Aᵗ x xᵗ y yᵗ p}
: p # xᵗ = yᵗ → eqᵗ A Aᵗ x xᵗ y yᵗ p.
Definition eqᵗ_eq_equiv A Aᵗ x xᵗ y yᵗ p
: eqᵗ A Aᵗ x xᵗ y yᵗ p <~> p # xᵗ = yᵗ.
Theorem UIP_provably_parametric : ∀ h : UIP, UIPᵗ h.
Definition wFunext
:= ∀ A (B : A → Type) (f g : ∀ x, B x), (∀ x, f x = g x) → f = g.
Theorem wFunext_provably_parametric : ∀ h : wFunext, wFunextᵗ h.
Definition wUnivalence := ∀ A B, A <~> B → A = B.
Theorem wUnivalence_provably_parametric : ∀ h, wUnivalenceᵗ h.
Definition equiv_paths {A B} (p : A = B) : A <~> B
:= transport (Equiv A) p equiv_idmap.
Definition Univalence := ∀ A B (p : A = B), IsEquiv (equiv_paths p).
Definition coe {A B} (p : A = B) : A → B := transport idmap p.
Definition Univalence' := ∀ A B (p : A = B), IsEquiv (coe p).
Definition UU' : Univalence' → Univalence.
Defined.
Lemma pathsᵗ_ok {A} {Aᵗ : A → Type} {x y} {xᵗ : Aᵗ y} (p : x = y)
: pathsᵗ A Aᵗ x (transport Aᵗ p^ xᵗ) y xᵗ p.
Lemma pathsᵗ_ok2 {A} {Aᵗ : A → Type} {x y} {xᵗ : Aᵗ y} (p q : x = y) e r
(Hr : e # (pathsᵗ_ok p) = r)
: pathsᵗ (x = y) (pathsᵗ A Aᵗ x (transport Aᵗ p^ xᵗ) y xᵗ) p (pathsᵗ_ok p) q r e.
Definition apᵗ_idmap {A} {Aᵗ : A → Type} {x y xᵗ yᵗ} (p : x = y)
(pᵗ : pathsᵗ A Aᵗ x xᵗ y yᵗ p)
: apᵗ A Aᵗ A Aᵗ idmap (fun u ⇒ idmap) x xᵗ y yᵗ p pᵗ = (ap_idmap p)^ # pᵗ.
Definition U'U : Univalence → Univalence'.
Defined.
Theorem Univalence'_provably_parametric : ∀ h : Univalence', Univalence'ᵗ h.
Definition Univalence_wFunext : Univalence → wFunext.
Admitted.
Theorem Univalence_provably_parametric : ∀ h : Univalence, Univalenceᵗ h.
End Axioms.