Skip to content

Instantly share code, notes, and snippets.

@codyroux codyroux/euclid.v
Last active Dec 31, 2015

Embed
What would you like to do?
Arithmetic, again
(* 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
You can’t perform that action at this time.