Library MetaCoq.Translations.standard_model

Infix "<=" := Nat.leb.

Definition default_term := tVar "constant_not_found".
Definition debug_term msg:= tVar ("debug: " ++ msg).

Print Typing Flags.


Fixpoint kproj (k : nat) (t : term) :=
  match k with
  | 0 ⇒ t
  | S k ⇒ kproj k (proj1 t)
  end.

Notation app0 := (fun t ⇒ subst_app t [tRel 0]).

Fixpoint tsl (ΣE : tsl_context) (Γ : context) (t : term) {struct t}
  : tsl_result term :=
  match t with
  | tSort s ⇒ Γ' <- tsl_ctx ΣE Γ ;;
              ret (tLambda (nNamed "γ") Γ' (tSort s))
  | tRel k ⇒ Γ' <- tsl_ctx ΣE Γ ;;
             ret (tLambda (nNamed "γ") Γ' (proj2 (kproj k (tRel 0))))
  
  | tCast t c A ⇒ Γ' <- tsl_ctx ΣE Γ ;;
                  t' <- tsl ΣE Γ t ;;
                  A' <- tsl ΣE Γ A ;;
                  ret (tLambda (nNamed "γ") Γ'
                               (tCast (app0 t') c (app0 A')))
  | tProd na A B ⇒ Γ' <- tsl_ctx ΣE Γ ;;
                   A' <- tsl ΣE Γ A ;;
                   B' <- tsl ΣE (Γ ,, vass na A) B ;;
                   ret (tLambda (nNamed "γ") Γ'
                                (tProd na (app0 A')
                                   (subst_app B' [pair Γ' A' (tRel 1) (tRel 0)])))
  | tLambda na A t ⇒ Γ' <- tsl_ctx ΣE Γ ;;
                     A' <- tsl ΣE Γ A ;;
                     t' <- tsl ΣE (Γ ,, vass na A) t ;;
                     ret (tLambda (nNamed "γ") Γ'
                            (tLambda na (app0 A')
                               (subst_app t' [pair Γ' (up A') (tRel 1) (tRel 0)])))
  | tLetIn na t A u ⇒ Γ' <- tsl_ctx ΣE Γ ;;
                      t' <- tsl ΣE Γ t ;;
                      A' <- tsl ΣE Γ A ;;
                      u' <- tsl ΣE (Γ ,, vdef na t A) u ;;
                      ret (tLambda (nNamed "γ") Γ' (tLetIn na t' A' u'))
  | tApp t lu ⇒ Γ' <- tsl_ctx ΣE Γ ;;
                t' <- tsl ΣE Γ t ;;
                lu' <- monad_map (tsl ΣE Γ) lu ;;
                ret (tLambda (nNamed "γ") Γ' (mkApps (app0 t') (map app0 lu')))
  
  
  
  
  | tConst s univs ⇒ Γ' <- tsl_ctx ΣE Γ ;;
                     t' <- lookup_tsl_table' (snd ΣE) (ConstRef s) ;;
                     ret (tLambda (nNamed "γ") Γ' (subst_app t' [ttt]))
  | tInd i univs ⇒ lookup_tsl_table' (snd ΣE) (IndRef i)
  | tConstruct i n univs ⇒ lookup_tsl_table' (snd ΣE) (ConstructRef i n)
  | tProj p t ⇒ Γ' <- tsl_ctx ΣE Γ ;;
                t' <- tsl ΣE Γ t ;;
                ret (tLambda (nNamed "γ") Γ' (tProj p t'))

  | _ ⇒ ret t
  end
with tsl_ctx (ΣE : tsl_context) (Γ : context) {struct Γ} : tsl_result term :=
       match Γ with
       | [] ⇒ ret tUnit
       | {| decl_body := None; decl_type := A |} :: Γ ⇒
            Γ' <- tsl_ctx ΣE Γ ;;
            A' <- tsl ΣE Γ A ;;
            ret (pack Γ' A')
       | _ ⇒ todo
       end.

Instance param : Translation :=
  {| tsl_id := tsl_ident ;
     tsl_tm := fun ΣE ⇒ tsl ΣE [] ;
     tsl_ty := Some (fun ΣE t ⇒ t' <- tsl ΣE [] t ;; ret (subst_app t' [ttt])) ;
     tsl_ind := todo |}.

Definition toto := fun (f : ∀ A, A → A) ⇒ f Type.
Goal nat.
Print totoᵗ.
Eval cbv delta beta in totoᵗ.

Definition FALSE := ∀ X, X.

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 Funext
    := ∀ A B (f g : ∀ x : A, B x), IsEquiv (@apD10 A B f g).


  Theorem wFunext_provably_parametric : ∀ h : Funext, Funextᵗ h.



Definition equiv_id A : isequiv A A (fun x ⇒ x).
Defined.



Lemma eq_rectᵗ : eq_rect_Typeᵗ eq_rect.

Definition TC' := (ConstRef "Coq.Init.Logic.eq_rect", tConst "eq_rectᵗ" []) :: TC.

Definition eq_to_iso A B : A = B → ∃ f, isequiv A B f.
Defined.

Definition UA := ∀ A B, isequiv _ _ (eq_to_iso A B).



Axiom ua : UA.

Goal UAᵗ ua.