Library HoTT_Tests.Tactics.EliminationSchemes

From HoTT.Basics Require Import Overture Notations.
From HoTT.Spaces Require Import Nat.Core Nat.Arithmetic SInt.

Local Set Warnings "-unknown-warning".
Local Set Warnings "+deprecated-lookup-elim-by-name".

Goal ∀ n : nat, n = n.
Proof.
  intro n; induction n; reflexivity.
Qed.

Goal ∀ (A : Type) (n : nat), A → A.
Proof.
  intros A n a; induction n; exact a.
Qed.

Goal Empty → Unit.
Proof.
  intro x; elim x.
Qed.

Goal ∀ A : Type, Empty → A.
Proof.
  intros A x; elim x.
Qed.

Goal ∀ n m (p : (n ≤ m)%nat), p = p.
Proof.
  intros n m p; induction p; reflexivity.
Qed.

Goal ∀ n m, increasing_geq n m → Unit.
Proof.
  intros n m p; induction p; exact tt.
Qed.

Goal ∀ x : SInt, x = x.
Proof.
  intro x; induction x; reflexivity.
Qed.

Goal ∀ (A : Type) (x : SInt), A → A.
Proof.
  intros A x a; induction x; exact a.
Qed.

(* These Unit-valued goals force elimination into Type0, exercising the rec_dep registrations. *)
Goal ∀ n : nat, Unit.
Proof.
  intro n; induction n; exact tt.
Qed.

Goal ∀ n m (p : (n ≤ m)%nat), Unit.
Proof.
  intros n m p; induction p; exact tt.
Qed.

Goal ∀ x : SInt, Unit.
Proof.
  intro x; induction x; exact tt.
Qed.