Peano_dec.v

(************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) (* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (* * (see LICENSE file for the text of the license) *) (************************************************************************) Require Import Decidable PeanoNat. Require Eqdep_dec. Local Open Scope nat_scope. Implicit Types m n x y : nat. Theorem O_or_S n : {m : nat | S m = n} + {0 = n}.

n:nat
{m : nat | S m = n} + {0 = n}

Proof.

n:nat
{m : nat | S m = n} + {0 = n}

induction n.

{m : nat | S m = 0} + {0 = 0}

n:nat
IHn:{m : nat | S m = n} + {0 = n}
{m : nat | S m = S n} + {0 = S n}

{m : nat | S m = 0} + {0 = 0}

now right. -

n:nat
IHn:{m : nat | S m = n} + {0 = n}
{m : nat | S m = S n} + {0 = S n}

left; exists n; auto. Defined. Notation eq_nat_dec := Nat.eq_dec (only parsing). Hint Resolve O_or_S eq_nat_dec: arith. Theorem dec_eq_nat n m : decidable (n = m).

n, m:nat
decidable (n = m)

Proof.

n, m:nat
decidable (n = m)

elim (Nat.eq_dec n m); [left|right]; trivial. Defined. Register dec_eq_nat as num.nat.eq_dec. Definition UIP_nat:= Eqdep_dec.UIP_dec Nat.eq_dec. Import EqNotations. Lemma le_unique: forall m n (le_mn1 le_mn2 : m <= n), le_mn1 = le_mn2.

forall (m n : nat) (le_mn1 le_mn2 : m <= n), le_mn1 = le_mn2

Proof.

forall (m n : nat) (le_mn1 le_mn2 : m <= n), le_mn1 = le_mn2

intros m n.

m, n:nat
forall le_mn1 le_mn2 : m <= n, le_mn1 = le_mn2

generalize (eq_refl (S n)).

m, n:nat
S n = S n -> forall le_mn1 le_mn2 : m <= n, le_mn1 = le_mn2

generalize n at -1.

m, n:nat
forall n0 : nat, S n = S n0 -> forall le_mn1 le_mn2 : m <= n0, le_mn1 = le_mn2

induction (S n) as [|n0 IHn0]; try discriminate.

m, n, n0:nat
IHn0:forall n1 : nat, n0 = S n1 -> forall le_mn1 le_mn2 : m <= n1, le_mn1 = le_mn2
forall n1 : nat, S n0 = S n1 -> forall le_mn1 le_mn2 : m <= n1, le_mn1 = le_mn2

clear n; intros n [= <-] le_mn1 le_mn2.

m, n0:nat
IHn0:forall n : nat, n0 = S n -> forall le_mn0 le_mn3 : m <= n, le_mn0 = le_mn3
le_mn1, le_mn2:m <= n0
le_mn1 = le_mn2

pose (def_n2 := eq_refl n0); transitivity (eq_ind _ _ le_mn2 _ def_n2).

m, n0:nat
IHn0:forall n : nat, n0 = S n -> forall le_mn0 le_mn3 : m <= n, le_mn0 = le_mn3
le_mn1, le_mn2:m <= n0
def_n2:=eq_refl:n0 = n0
le_mn1 = eq_ind n0 (le m) le_mn2 n0 def_n2

m, n0:nat
IHn0:forall n : nat, n0 = S n -> forall le_mn0 le_mn3 : m <= n, le_mn0 = le_mn3
le_mn1, le_mn2:m <= n0
def_n2:=eq_refl:n0 = n0
eq_ind n0 (le m) le_mn2 n0 def_n2 = le_mn2

2: reflexivity.

m, n0:nat
IHn0:forall n : nat, n0 = S n -> forall le_mn0 le_mn3 : m <= n, le_mn0 = le_mn3
le_mn1, le_mn2:m <= n0
def_n2:=eq_refl:n0 = n0
le_mn1 = eq_ind n0 (le m) le_mn2 n0 def_n2

generalize def_n2; revert le_mn1 le_mn2.

m, n0:nat
IHn0:forall n : nat, n0 = S n -> forall le_mn1 le_mn2 : m <= n, le_mn1 = le_mn2
def_n2:=eq_refl:n0 = n0
forall (le_mn1 le_mn2 : m <= n0) (def_n0 : n0 = n0), le_mn1 = eq_ind n0 (le m) le_mn2 n0 def_n0

generalize n0 at 1 4 5 7; intros n1 le_mn1.

m, n0:nat
IHn0:forall n : nat, n0 = S n -> forall le_mn0 le_mn2 : m <= n, le_mn0 = le_mn2
def_n2:=eq_refl:n0 = n0
n1:nat
le_mn1:m <= n1
forall (le_mn2 : m <= n0) (def_n0 : n0 = n1), le_mn1 = eq_ind n0 (le m) le_mn2 n1 def_n0

destruct le_mn1; intros le_mn2; destruct le_mn2.

m:nat
IHn0:forall n : nat, m = S n -> forall le_mn1 le_mn2 : m <= n, le_mn1 = le_mn2
def_n2:=eq_refl:m = m
forall def_n0 : m = m, le_n m = eq_ind m (le m) (le_n m) m def_n0

m, m0:nat
IHn0:forall n : nat, S m0 = S n -> forall le_mn1 le_mn0 : m <= n, le_mn1 = le_mn0
def_n2:=eq_refl:S m0 = S m0
le_mn2:m <= m0
forall def_n0 : S m0 = m, le_n m = eq_ind (S m0) (le m) (le_S m m0 le_mn2) m def_n0

m:nat
IHn0:forall n : nat, m = S n -> forall le_mn0 le_mn2 : m <= n, le_mn0 = le_mn2
def_n2:=eq_refl:m = m
m0:nat
le_mn1:m <= m0
forall def_n0 : m = S m0, le_S m m0 le_mn1 = eq_ind m (le m) (le_n m) (S m0) def_n0

m, m1:nat
IHn0:forall n : nat, S m1 = S n -> forall le_mn0 le_mn3 : m <= n, le_mn0 = le_mn3
def_n2:=eq_refl:S m1 = S m1
m0:nat
le_mn1:m <= m0
le_mn2:m <= m1
forall def_n0 : S m1 = S m0, le_S m m0 le_mn1 = eq_ind (S m1) (le m) (le_S m m1 le_mn2) (S m0) def_n0

m:nat
IHn0:forall n : nat, m = S n -> forall le_mn1 le_mn2 : m <= n, le_mn1 = le_mn2
def_n2:=eq_refl:m = m
forall def_n0 : m = m, le_n m = eq_ind m (le m) (le_n m) m def_n0

now intros def_n0; rewrite (UIP_nat _ _ def_n0 eq_refl). +

m, m0:nat
IHn0:forall n : nat, S m0 = S n -> forall le_mn1 le_mn0 : m <= n, le_mn1 = le_mn0
def_n2:=eq_refl:S m0 = S m0
le_mn2:m <= m0
forall def_n0 : S m0 = m, le_n m = eq_ind (S m0) (le m) (le_S m m0 le_mn2) m def_n0

intros def_n0; generalize le_mn2; rewrite <-def_n0; intros le_mn0.

m, m0:nat
IHn0:forall n : nat, S m0 = S n -> forall le_mn1 le_mn3 : m <= n, le_mn1 = le_mn3
def_n2:=eq_refl:S m0 = S m0
le_mn2:m <= m0
def_n0:S m0 = m
le_mn0:S m0 <= m0
le_n (S m0) = eq_ind (S m0) (le (S m0)) (le_S (S m0) m0 le_mn0) (S m0) eq_refl

now destruct (Nat.nle_succ_diag_l _ le_mn0). +

m:nat
IHn0:forall n : nat, m = S n -> forall le_mn0 le_mn2 : m <= n, le_mn0 = le_mn2
def_n2:=eq_refl:m = m
m0:nat
le_mn1:m <= m0
forall def_n0 : m = S m0, le_S m m0 le_mn1 = eq_ind m (le m) (le_n m) (S m0) def_n0

intros def_n0; generalize le_mn1; rewrite def_n0; intros le_mn0.

m:nat
IHn0:forall n : nat, m = S n -> forall le_mn2 le_mn3 : m <= n, le_mn2 = le_mn3
def_n2:=eq_refl:m = m
m0:nat
le_mn1:m <= m0
def_n0:m = S m0
le_mn0:S m0 <= m0
le_S (S m0) m0 le_mn0 = eq_ind (S m0) (le (S m0)) (le_n (S m0)) (S m0) eq_refl

now destruct (Nat.nle_succ_diag_l _ le_mn0). +

m, m1:nat
IHn0:forall n : nat, S m1 = S n -> forall le_mn0 le_mn3 : m <= n, le_mn0 = le_mn3
def_n2:=eq_refl:S m1 = S m1
m0:nat
le_mn1:m <= m0
le_mn2:m <= m1
forall def_n0 : S m1 = S m0, le_S m m0 le_mn1 = eq_ind (S m1) (le m) (le_S m m1 le_mn2) (S m0) def_n0

intros def_n0.

m, m1:nat
IHn0:forall n : nat, S m1 = S n -> forall le_mn0 le_mn3 : m <= n, le_mn0 = le_mn3
def_n2:=eq_refl:S m1 = S m1
m0:nat
le_mn1:m <= m0
le_mn2:m <= m1
def_n0:S m1 = S m0
le_S m m0 le_mn1 = eq_ind (S m1) (le m) (le_S m m1 le_mn2) (S m0) def_n0

injection def_n0 as ->.

m, m0:nat
def_n2:=eq_refl:S m0 = S m0
IHn0:forall n : nat, S m0 = S n -> forall le_mn0 le_mn3 : m <= n, le_mn0 = le_mn3
le_mn1:m <= m0
def_n0:S m0 = S m0
le_mn2:m <= m0
le_S m m0 le_mn1 = eq_ind (S m0) (le m) (le_S m m0 le_mn2) (S m0) def_n0

rewrite (UIP_nat _ _ def_n0 eq_refl); simpl.

m, m0:nat
def_n2:=eq_refl:S m0 = S m0
IHn0:forall n : nat, S m0 = S n -> forall le_mn0 le_mn3 : m <= n, le_mn0 = le_mn3
le_mn1:m <= m0
def_n0:S m0 = S m0
le_mn2:m <= m0
le_S m m0 le_mn1 = le_S m m0 le_mn2

assert (H : le_mn1 = le_mn2).

m, m0:nat
def_n2:=eq_refl:S m0 = S m0
IHn0:forall n : nat, S m0 = S n -> forall le_mn0 le_mn3 : m <= n, le_mn0 = le_mn3
le_mn1:m <= m0
def_n0:S m0 = S m0
le_mn2:m <= m0
le_mn1 = le_mn2

m, m0:nat
def_n2:=eq_refl:S m0 = S m0
IHn0:forall n : nat, S m0 = S n -> forall le_mn0 le_mn3 : m <= n, le_mn0 = le_mn3
le_mn1:m <= m0
def_n0:S m0 = S m0
le_mn2:m <= m0
H:le_mn1 = le_mn2
le_S m m0 le_mn1 = le_S m m0 le_mn2

now apply IHn0.

m, m0:nat
def_n2:=eq_refl:S m0 = S m0
IHn0:forall n : nat, S m0 = S n -> forall le_mn0 le_mn3 : m <= n, le_mn0 = le_mn3
le_mn1:m <= m0
def_n0:S m0 = S m0
le_mn2:m <= m0
H:le_mn1 = le_mn2
le_S m m0 le_mn1 = le_S m m0 le_mn2

now rewrite H. Qed.