Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
An arithmetic development that uses equality over Type rather than Prop.
(* 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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.