An arithmetic development that uses equality over Type rather than Prop.

a_little_arithmetic.v

(* Sigma types *)

(* Inductive Sigma (A:Set)(B:A -> Set) :Set := Spair: forall a:A, forall b : B a,Sigma A B. *)

(* Definition E (A:Set)(B:A -> Set) (C: Sigma A B -> Set) (c: Sigma A B)  *)
(*   (d: (forall x:A, forall y:B x, C (Spair A B x y))): C c := *)
(*   match c as c0 return (C c0) with  *)
(*     | Spair a b => d a b  *)
(*   end. *)

Print sigT.

(* Binary sum type *)

(* Inductive sum' (A B:Set):Set := inl': A -> sum' A B | inr': B -> sum' A B. *)

(* Print sum'_rect. *)

(* Definition D (A B : Set)(C: sum' A B -> Set) (c: sum' A B)  *)
(*   (d: (forall x:A, C (inl' A B x))) (e: (forall y:B, C (inr' A B y))): C c := *)
(*   match c as c0 return C c0 with  *)
(*     | inl' x => d x  *)
(*     | inr' y => e y  *)
(*   end. *)

Print sum.

(* Three useful finite sets *)

(* Inductive N_0: Set :=. *)

(* Definition R_0 (C:N_0 -> Set) (c: N_0): C c :=  *)
(*   match c as c0 return (C c0) with end. *)

Print False.


(* Inductive N_1: Set :=  *)
(*   zero_1 : N_1. *)

(* Definition R_1 (C:N_1 -> Set) (c: N_1) (d_zero: C zero_1): C c :=  *)
(*   match c as c0 return (C c0) with  *)
(*     | zero_1 => d_zero  *)
(*   end. *)

Print unit.


(* Inductive N_2: Set :=  *)
(*  | zero_2 : N_2  *)
(*  | one_2 : N_2. *)

(* Definition R_2 (C:N_2 -> Set) (c: N_2) (d_zero: C zero_2) (d_one: C one_2): C c :=  *)
(*   match c as c0 return (C c0) with  *)
(*     | zero_2 => d_zero  *)
(*     | one_2 => d_one  *)
(*   end. *)

Print bool.

(* Natural numbers *)

(* Inductive N:Set :=  *)
(* |zero: N  *)
(* | succ : N -> N. *)

(* Print N. *)

(* Print N_rect. *)

(* Definition R (C:N -> Set) (d: C zero) (e: (forall x:N, C x -> C (succ x))): (forall n:N, C n) :=  *)
(*   fix F (n: N): C n :=  *)
(*   match n as n0 return (C n0) with  *)
(*     | zero => d  *)
(*     | succ n0 => e n0 (F n0)  *)
(*   end. *)

Print nat.

(* Boolean to truth-value converter *)

(* Definition Tr (c:N_2) : Set :=  *)
(*   match c as c0 with  *)
(*     | zero_2 => N_0  *)
(*     | one_2 => N_1  *)
(*   end. *)

Definition Tr (b : bool) : Type := if b then unit else False.

(* Identity type *)

(* Inductive I {A: Type}(x: A) : A -> Type :=  *)
(*   r : I x x. *)

(* Print I_rect. *)

(* Hint Resolve r.  *)

Print identity.

Notation "x ~ y" := (identity x y)(at level 60).

Notation "#":=(identity_refl)(at level 10).

Definition J 
  (A : Type)
  (C: (forall x y : A, forall e : x ~ y, Type)) 
  (d: (forall x:A, C x x (# x))) :
  (forall (a : A)(b : A)(e : a ~ b),  C a b e) :=
    fun a b e =>
      match e in _ ~ b with
        | # => d a
      end.

Check J.

(* functions are extensional wrt identity types *)

Definition id_ext {A B: Type} {x y : A} (f: A -> B): 
  (x ~ y -> (f x) ~ (f y))
  := fun p =>
    match p with
      # => # (f x)
    end.

(* addition *)

(* Definition add (m n:N) : N := R (fun z=> N) m (fun x y => succ y) n. *)

Print plus.

(* multiplication *)

(* Definition mul (m n:N) : N := R (fun z=> N) zero (fun x y => add y m) n. *)

Print mult.

(* Axioms of Peano verified *)

Require Import Arith.

Theorem P1a: (forall x: nat, (0 + x) ~ x).
Proof.
  simpl; auto.
Defined.


Theorem P1b: forall x y: nat, ((S x) + y) ~ (S (x + y)).
Proof.
  simpl; auto.
Defined.

Theorem P2a: (forall x: nat, (0 * x) ~ 0).
Proof.
  simpl; auto.
Defined.

Theorem P2b: forall x y: nat, ((S x) * y) ~ (y + (x * y)).
Proof.
  simpl; auto.
Defined.

(* Definition pd (n: N): N := R (fun _=> N) zero (fun x y=> x) n. *)

Print pred.

Theorem P3: (forall x y: nat, (S x) ~ (S y) -> x ~ y).
Proof.
 intros x y p.
 apply (id_ext pred p).
Defined.

(* Definition not (A:Set): Set:= (A -> N_0). *)

Print notT.

Definition isnonzero (n: nat): bool:= if n then false else true.

Eval compute in isnonzero 1.
Eval compute in isnonzero 0.

Notation "x !~ y":= (notT (x ~ y))(at level 60).

Definition false_if_succ (n : nat) : Type := if n then unit else False.

Hint Resolve tt.

Theorem P4 : (forall x: nat, (S x) !~ 0).
Proof.
  intro x.
  intro.
  assert (false_if_succ (S x)).
  rewrite H.
  simpl; auto.
  simpl in X; auto.
Qed.


Theorem P5 (P:nat -> Type): P 0 -> (forall x:nat, P x -> P (S x)) -> (forall x:nat, P x).
Proof.
  intros; induction x; auto.
Defined.

(* I(A,-,-) is an equivalence relation *)

(*All these are in the std library *)

Lemma Ireflexive (A:Set): (forall x:A, x ~ x).
Proof.
  auto.
Defined.

Lemma Isymmetric (A:Set): (forall x y:A, x ~ y -> y ~ x).
Proof.
  auto.
Defined.

Lemma Itransitive (A:Set): (forall x y z:A, x ~ y -> y ~ z -> x ~ z).
Proof.
  intros x y z e1 e2.
  rewrite e1; auto.
Defined.

Lemma S_cong : (forall m n:nat, m ~ n -> (S m) ~ (S n)).
Proof.
  intros m n e; rewrite e; auto.
Defined.

Lemma zeroadd: (forall n:nat, (n + 0) ~ n).
Proof.
  induction n; simpl; auto.
  rewrite IHn; auto.
Defined.

Hint Rewrite zeroadd.

Lemma Sadd: (forall m n:nat, (m + (S n)) ~ (S (m + n))).
Proof.
  induction m; intro n; auto.
  simpl; rewrite IHm; auto.
Defined.

Hint Rewrite Sadd.

Lemma commutative_add: (forall m n:nat, (m + n) ~ (n + m)).
Proof.
  induction m; intro n.
  rewrite zeroadd; auto.
  simpl; rewrite IHm.
  rewrite Sadd; auto.
Defined.

Lemma associative_add: (forall m n k:nat, ((m + n) + k) ~ (m + (n + k))).
Proof.
  induction m; auto.
  intros n k; simpl.
  rewrite IHm; auto.
Defined.

Print sum.

Open Scope type_scope.

(* Definition or (A B : Set):= (A + B). *)

Definition less (m n: nat) := { z : nat & S (z + m) ~ n}.

Notation "m < n" := (less m n)(at level 70).

Lemma less_lem : forall n m : nat, n < (S m) -> (n < m) + (n ~ m).
Proof.
  intros n m leq.
  elim leq.
  induction x; simpl; intro e.
  right.
  apply P3; auto.
  left.
  exists x.
  apply P3; auto.
Defined.


Theorem nattrichotomy: forall n m:nat, (n < m) + (n ~ m) + (m < n).
Proof.
  induction n; induction m; simpl.
  left; right; auto.
  left; left.
  exists m; rewrite zeroadd; auto.
  right; exists n; rewrite zeroadd; auto.
  destruct IHm as [ leq | gt ].
  destruct leq as [lt | eq].
  left; left; destruct lt.
  exists (S x).
  simpl; rewrite i; auto.
  left; left; exists 0.
  rewrite eq; simpl; auto.
  generalize (less_lem _ _ gt); intro less_eq.
  destruct less_eq as [less| eq].
  right.
  destruct less.
  exists x.
  rewrite Sadd; rewrite<- i; auto.
  left;right; rewrite eq; auto.
Defined.