Last active
December 31, 2015 04:29
-
-
Save codyroux/7934436 to your computer and use it in GitHub Desktop.
Arithmetic, again
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(* Cleanup and proofs of user11942s code *) | |
Print sigT. | |
Print sum. | |
Print False. | |
Print unit. | |
Print bool. | |
Print nat. | |
Definition Tr (b : bool) : Type := if b then unit else False. | |
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. | |
Print plus. | |
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. | |
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. | |
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. | |
(* ~ 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. | |
Lemma zeromul : forall n : nat, n * 0 ~ 0. | |
Proof. | |
induction n; simpl; auto. | |
Qed. | |
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. | |
right; left; auto. | |
left. | |
exists m; rewrite zeroadd; auto. | |
right; right; exists n; rewrite zeroadd; auto. | |
destruct IHm as [ lt | [eq | gt] ]. | |
left; destruct lt. | |
exists (S x). | |
simpl; rewrite i; auto. | |
left; exists 0. | |
rewrite eq; simpl; auto. | |
generalize (less_lem _ _ gt); intro less_eq. | |
destruct less_eq as [less| eq]. | |
right; right. | |
destruct less. | |
exists x. | |
rewrite Sadd; rewrite<- i; auto. | |
right; left; rewrite eq; auto. | |
Defined. | |
Lemma not_lt_zero : forall n, notT (n < 0). | |
Proof. | |
intros n lt. | |
destruct lt. | |
eapply P4; apply i. | |
Defined. | |
Lemma lt_suc : forall n m, n < m -> S n < S m. | |
Proof. | |
intros n m lt. | |
destruct lt. | |
exists x; simpl. | |
rewrite Sadd. | |
rewrite i; auto. | |
Defined. | |
Lemma suc_lt : forall n m, S n < S m -> n < m. | |
Proof. | |
intros n m lt. | |
destruct lt. | |
exists x; simpl. | |
rewrite Sadd in i. | |
apply P3; auto. | |
Defined. | |
Lemma lt_suc_r : forall n m, n < m -> n < (S m). | |
Proof. | |
induction n; induction m; intro lt. | |
exists 0; auto. | |
exists (S m); rewrite zeroadd; auto. | |
exfalso; eapply not_lt_zero; apply lt. | |
apply lt_suc; apply IHn. | |
apply suc_lt; auto. | |
Defined. | |
(* Acc is a datatype that captures well-foundedness *) | |
Print Acc. | |
Print well_founded. | |
(* We redo the definitions to eliminate to Type *) | |
Inductive Acc {A : Type} (R : A -> A -> Type) (x : A) : Type := | |
Acc_intro : (forall y : A, R y x -> Acc R y) -> Acc R x. | |
Print Acc_rect. | |
Definition well_founded {A : Type} R := forall x : A, Acc R x. | |
Theorem wf_lt : well_founded less. | |
Proof. | |
unfold well_founded. | |
induction x; apply Acc_intro. | |
intros y lt. | |
destruct lt. | |
(* slight trick here: inversion tells us no such i can exist *) | |
inversion i. | |
intros y lt. | |
(* You don't even need trichotomy here! This is another 'benefit' of formalization: | |
it tends to force you to minimize extraneous lemmas/hypotheses *) | |
generalize (less_lem y x lt); intros [lt_x | eq]. | |
destruct IHx as (ind); apply ind; auto. | |
rewrite eq; auto. | |
Defined. | |
(* The division algorithm, by well-founded induction on wf_lt *) | |
Print minus. | |
Lemma lt_minus : forall n m, (S n) - (S m) < (S n). | |
Proof. | |
simpl. | |
induction n; induction m; simpl; auto. | |
exists 0; auto. | |
exists 0; auto. | |
apply lt_suc_r; auto. | |
Defined. | |
Definition euclid (n d : nat) := | |
{ q : nat & { r : nat & ((n ~ ((S d)*q + r))%nat * (r < (S d)))%type }}. | |
Close Scope type. | |
Lemma add_assoc : forall m n k, (n + m) + k ~ n + (m + k). | |
Proof. | |
induction n; induction m; intro k; simpl; auto. | |
rewrite zeroadd; auto. | |
rewrite IHn; simpl. | |
auto. | |
Defined. | |
Lemma add_comm : forall m n, n + m ~ m + n. | |
Proof. | |
induction n; induction m; simpl; auto. | |
rewrite zeroadd; auto. | |
rewrite zeroadd; auto. | |
rewrite IHn. | |
rewrite Sadd; auto. | |
Defined. | |
Lemma Smul : forall n m, n * (S m) ~ n + n * m. | |
Proof. | |
induction n; simpl; auto. | |
intro m. | |
rewrite IHn; auto. | |
apply id_ext. | |
rewrite<- add_assoc. | |
rewrite<- add_assoc. | |
rewrite (add_comm n m); auto. | |
Defined. | |
Theorem minus_swap : forall n m k, m < n -> n - m ~ k -> n ~ k + m. | |
Proof. | |
induction n. | |
intros m k lt eq. | |
exfalso. | |
apply (not_lt_zero _ lt). | |
induction m; intros; auto. | |
simpl in H0; rewrite H0; rewrite zeroadd; auto. | |
rewrite Sadd. | |
apply id_ext. | |
apply IHn. | |
apply suc_lt; auto. | |
simpl in H0. | |
auto. | |
Defined. | |
Theorem minus_eq : forall n, n - n ~ 0. | |
Proof. | |
induction n; simpl; auto. | |
Defined. | |
Definition div_rem (n d : nat) : euclid n d. | |
Proof. | |
(*New trick here: the refine tactic, | |
that allows writing programs with pieces of proofs in them *) | |
Print Acc_rect. | |
refine ( | |
(fix Div (n d : nat) (wf_n : Acc less n) {struct wf_n} : euclid n d := | |
let m := S d in | |
match wf_n with | |
| Acc_intro acc_lt_n => | |
match nattrichotomy n m with | |
| inl lt_n_m => existT _ 0 (existT _ n _) | |
| inr eq_or_gt => | |
match Div (n - m) d (acc_lt_n (n - m) _) with | |
| existT q' (existT r' prop) => existT _ (S q') (existT _ r' _) | |
end | |
end | |
end) n d (wf_lt n)). | |
simpl. | |
rewrite zeromul. | |
simpl; split; auto. | |
induction n0; auto. | |
exfalso. | |
destruct eq_or_gt. | |
eapply P4; symmetry; exact i. | |
eapply not_lt_zero; exact l. | |
(* apply acc_lt_n. *) | |
apply lt_minus. | |
destruct s. | |
destruct prop. | |
destruct p. | |
split. | |
simpl. | |
subst m. | |
simpl in i. | |
destruct eq_or_gt. | |
rewrite i1 in i0. | |
rewrite i1 in i. | |
rewrite Smul. | |
simpl in i0. | |
rewrite minus_eq in i0. | |
rewrite minus_eq in i. | |
rewrite i1. | |
apply id_ext. | |
rewrite<- add_assoc. | |
rewrite add_assoc. | |
(*cheat *) | |
replace (q' + d0 + (d0 * q' + r')) with (d0 + (q' + d0 * q' + r')). | |
rewrite<- i. | |
rewrite zeroadd; auto. | |
Require Import Omega. | |
omega. | |
generalize (minus_swap _ _ _ l1 i). | |
intro. | |
rewrite Smul. | |
assert (q' + d0 * q' + r' + S d0 = S (q' + (d0 + d0 * q') + r')) by omega. | |
rewrite<- H0; auto. | |
auto. | |
Defined. | |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment