Library MetaCoq.Translations.times_bool_fun

Record prod A B := pair { π1 : A ; π2 : B }.


Notation "( x ; y )" := (pair x y) : prod_scope.
Notation " A × B " := (prod A B) : type_scope.

Definition prod_ind := Eval compute in
  match tprod with tInd i _ ⇒ i | _ ⇒ mkInd "bug: prod not an inductive" 0 end.
Definition proj1 (t : term) : term
  := tProj (prod_ind, 2, 0) t.
Definition proj2 (t : term) : term
  := tProj (prod_ind, 2, S 0) t.

Definition timesBool (A : term) := tApp tprod [A; tbool].
Definition pairTrue typ tm := tApp tpair [typ; tbool; tm; ttrue].


Fixpoint tsl_rec (fuel : nat) (Σ : global_env_ext) (E : tsl_table) (Γ : context) (t : term) {struct fuel}
  : tsl_result term :=
  match fuel with
  | O ⇒ raise NotEnoughFuel
  | S fuel ⇒
  match t with
  | tRel n ⇒ ret (tRel n)
  | tSort s ⇒ ret (tSort s)

  | tCast t c A ⇒ t' <- tsl_rec fuel Σ E Γ t ;;
                  A' <- tsl_rec fuel Σ E Γ A ;;
                  ret (tCast t' c A')

  | tProd n A B ⇒ A' <- tsl_rec fuel Σ E Γ A ;;
                  B' <- tsl_rec fuel Σ E (Γ ,, vass n A) B ;;
                  ret (timesBool (tProd n A' B'))

  | tLambda n A t ⇒ A' <- tsl_rec fuel Σ E Γ A ;;
                    t' <- tsl_rec fuel Σ E (Γ ,, vass n A) t ;;
                    match infer' Σ (Γ ,, vass n A) t with
                    | Checked B ⇒
                      B' <- tsl_rec fuel Σ E (Γ ,, vass n A) B ;;
                      ret (pairTrue (tProd n A' B') (tLambda n A' t'))
                    | TypeError t ⇒ raise (TypingError t)
                    end

  | tLetIn n t A u ⇒ t' <- tsl_rec fuel Σ E Γ t ;;
                     A' <- tsl_rec fuel Σ E Γ A ;;
                     u' <- tsl_rec fuel Σ E (Γ ,, vdef n t A) u ;;
                     ret (tLetIn n t' A' u')

  | tApp t us ⇒ t' <- tsl_rec fuel Σ E Γ t ;;
                monad_fold_left (fun t u ⇒ u' <- tsl_rec fuel Σ E Γ u ;;
                                         ret (tApp (proj1 t) [u'])) us t'

  | tConst s univs ⇒ lookup_tsl_table' E (ConstRef s)
  | tInd i univs ⇒ lookup_tsl_table' E (IndRef i)
  | tConstruct i n univs ⇒ lookup_tsl_table' E (ConstructRef i n)
  | tProj p t ⇒ t' <- tsl_rec fuel Σ E Γ t ;;
                ret (tProj p t')

  | tFix bodies n ⇒
    Γ' <- monad_map (fun '{| dname := na; dtype := ty; dbody := b; rarg := r |} ⇒
                      ty' <- tsl_rec fuel Σ E Γ ty ;;
                      ret {| decl_name := na; decl_body := None; decl_type := ty'|})
                   bodies;;
    bodies' <- monad_map (fun '{| dname := na; dtype := ty; dbody := b; rarg := r |} ⇒
                           ty' <- tsl_rec fuel Σ E Γ ty ;;
                           b' <- tsl_rec fuel Σ E (Γ ++ Γ')%list b ;;
                           ret {| dname := na; dtype := ty';
                                  dbody := b'; rarg := r |})
                        bodies ;;
    ret (tFix bodies' n)
  | _ ⇒ raise TranslationNotHandeled
  end
  end.


Definition combine' {A B} (p : list A × list B) : list (A × B)
  := List.combine (fst p) (snd p).

Fixpoint replace pat u t {struct t} :=
  if eq_term uGraph.init_graph t pat then u else
    match t with
    | tCast t c A ⇒ tCast (replace pat u t) c (replace pat u A)
    | tProd n A B ⇒ tProd n (replace pat u A) (replace (up pat) (up u) B)
    | tLambda n A t ⇒ tLambda n (replace pat u A) (replace (up pat) (up u) t)
    | tLetIn n t A B ⇒ tLetIn n (replace pat u t) (replace pat u A)
                              (replace (up pat) (up u) B)
    | tApp t us ⇒ tApp (replace pat u t) (List.map (replace pat u) us)
    | tProj p t ⇒ tProj p (replace pat u 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.

Definition pouet (tm typ : term) : term.
Defined.

Definition tsl_mind_body (ΣE : tsl_context) (mp : string) (kn : kername)
           (mind : mutual_inductive_body)
  : tsl_result (tsl_table × list mutual_inductive_body).
Defined.

Fixpoint refresh_universes (t : term) {struct t} :=
  match t with
  | tSort s ⇒ tSort (if Universe.is_level s then s else fresh_universe)
  | tProd na b t ⇒ tProd na b (refresh_universes t)
  | tLetIn na b t' t ⇒ tLetIn na b t' (refresh_universes t)
  | tCast x x0 x1 ⇒ tCast (refresh_universes x) x0 (refresh_universes x1)
  | tLambda x x0 x1 ⇒ tLambda x (refresh_universes x0) (refresh_universes x1)
  | tApp x x0 ⇒ tApp (refresh_universes x) (List.map refresh_universes x0)
  | tProj x x0 ⇒ tProj x (refresh_universes x0)
  | _ ⇒ t
  end.

Instance tsl_fun : Translation
  := {| tsl_id := tsl_ident ;
        tsl_tm := fun ΣE t ⇒ t' <- tsl_rec fuel (fst ΣE) (snd ΣE) [] t ;;
                           ret (refresh_universes t');
        tsl_ty := Some (fun ΣE t ⇒ t' <- tsl_rec fuel (fst ΣE) (snd ΣE) [] t ;;
                                 ret (refresh_universes t')) ;
        tsl_ind := tsl_mind_body |}.

Tactic Notation "tSpecialize" ident(H) uconstr(t)
  := apply π1 in H; specialize (H t).
Tactic Notation "tIntro" ident(H)
  := refine (fun H ⇒ _; true).

Definition NotFunext :=
  ((∀ (A B : Set) (f g : A → B), (∀ x:A, f x = g x) → f = g) → False).






Definition UIP := ∀ A (x y : A) (p q : x = y), p = q.



Definition eqᵗ_eq {A} x y
  : eqᵗ A x y → x = y.

Definition eq_eqᵗ {A} x y
  : x = y → eqᵗ A x y.

Definition isequiv_eqᵗ_eq {A} x y
  : IsEquiv (@eqᵗ_eq A x y).

Theorem preserves_UIP : UIP → UIPᵗ.

Definition wFunext
  := ∀ A (B : A → Type) (f g : ∀ x, B x), (∀ x, f x = g x) → f = g.


Definition wUnivalence
  := ∀ A B, Equiv A B → A = B.



Theorem preserves_wUnivalence : wUnivalence → wUnivalenceᵗ.

Definition bool_of_Equivᵗ {A B} (e : Equivᵗ A B) : bool.
Defined.

Definition UA := ∀ A B, IsEquiv (paths_ind A (fun B _ ⇒ Equiv A B) (equiv_idmap A) B).


Axiom fx : Funext.
Axiom ua : UA.

Lemma eqᵗ_unit_unit (e e' : eqᵗ Type unit unit) : e = e'.