CoRN.logic.CLogic



Require Export Compare_dec.
Require Export CornBasics.
Require Export ZArith.
Require Export ZArithRing.
Require Export Div2.
Require Export Wf_nat.

Set Automatic Introduction.

Extending the Coq Logic

Because notions of apartness and order have computational meaning, we will have to define logical connectives in Type. In order to keep a syntactic distinction between types of terms, we define CProp as an alias for Type, to be used as type of (computationally meaningful) propositions.
Falsehood and negation will typically not be needed in CProp, as they are used to refer to negative statements, which carry no computational meaning. Therefore, we will simply define a negation operator from Type to Prop .
Conjunction, disjunction and existential quantification will have to come in multiple varieties. For conjunction, we will need four operators of type s1s2s3, where s3 is Prop if both s1 and s2 are Prop and CProp otherwise. We here take advantage of the inclusion of Prop in Type.
Disjunction is slightly different, as it will always return a value in CProp even if both arguments are propositions. This is because in general it may be computationally important to know which of the two branches of the disjunction actually holds.
Existential quantification will similarly always return a value in CProp.
  • CProp-valued conjuction will be denoted as and;
  • Crop-valued conjuction will be denoted as or;
  • Existential quantification will be written as {x:A & B} or {x:A | B},
according to whether B is respectively of type CProp or Prop.
In a few specific situations we do need truth, false and negation in CProp, so we will also introduce them; this should be a temporary option.
Finally, for other formulae that might occur in our CProp-valued propositions, such as (le m n), we have to introduce a CProp-valued version.

Notation "'CProp'":= Type.

Section Basics.

Basics

Here we treat conversion from Prop to CProp and vice versa, and some basic connectives in CProp.

Definition True_constr := I.

Definition ~ (P : CProp) := P.

Definition (A B : CProp) : CProp := prod (AB) (BA).

Definition proj1_sigT (A : Type) (P : ACProp) (e : sigT P) :=
  match e with
  | existT a ba
  end.

Definition proj2_sigT (A : Type) (P : ACProp) (e : sigT P) :=
  match e return (P (proj1_sigT A P e)) with
  | existT a bb
  end.

Inductive sig2T (A : Type) (P Q : ACProp) : CProp :=
    exist2T : x : A, P xQ xsig2T A P Q.

Definition proj1_sig2T (A : Type) (P Q : ACProp) (e : sig2T A P Q) :=
  match e with
  | exist2T a b ca
  end.

Definition proj2a_sig2T (A : Type) (P Q : ACProp) (e : sig2T A P Q) :=
  match e return (P (proj1_sig2T A P Q e)) with
  | exist2T a b cb
  end.

Definition proj2b_sig2T (A : Type) (P Q : ACProp) (e : sig2T A P Q) :=
  match e return (Q (proj1_sig2T A P Q e)) with
  | exist2T a b cc
  end.

End Basics.


Some lemmas to make it possible to use Step when reasoning with bi-implications.

Lemma Iff_left :
   (A B C : CProp),
  (A IFF B) → (A IFF C) → (C IFF B).
Proof.
 unfold .
 intuition.
Qed.

Lemma Iff_right:
   (A B C : CProp),
  (A IFF B) → (A IFF C) → (B IFF C).
Proof.
 unfold .
 intuition.
Qed.

Lemma Iff_refl : (A : CProp), (A IFF A).
Proof.
 unfold .
 intuition.
Qed.

Lemma Iff_sym :
   (A B : CProp),(A IFF B) → (B IFF A).
Proof.
 unfold .
 intuition.
Qed.

Lemma Iff_trans :
   (A B C : CProp),
  (prod (A IFF B) (B IFF C)) → (A IFF C).
Proof.
 unfold .
 intuition.
Qed.

Lemma Iff_imp_imp :
   (A B : CProp),
  (A IFF B) → (prod (AB) (BA)).
Proof.
 unfold .
 intuition.
Qed.

Declare Right Step Iff_right.
Declare Left Step Iff_left.
Hint Resolve Iff_trans Iff_sym Iff_refl Iff_right Iff_left Iff_imp_imp : algebra.

Lemma not_r_cor_rect :
   (A B : CProp) (S : Type) (l r : S),
  ~ B
   H : A or B,
  @sum_rect A B (fun _ : A or BS) (fun x : Al) (fun x : Br) H = l.
Proof.
 intros. elim H0.
 intros. reflexivity.
  intro. elim H. assumption.
Qed.

Lemma not_l_cor_rect :
   (A B : CProp) (S : Type) (l r : S),
  ~ A
   H : A or B,
  @sum_rect A B (fun _ : A or BS) (fun x : Al) (fun x : Br) H = r.
Proof.
 intros. elim H0.
 intro. elim H. assumption.
  intros. reflexivity.
Qed.


Hint Resolve pair inl inr existT exist2T : core.

Section Choice.

Variable P : natnatProp.

Lemma choice :
  ( n : nat, {m : nat | P n m}) →
  {d : natnat | n : nat, P n (d n)}.
Proof.
 intro H.
  (fun i : natproj1_sigT _ _ (H i)).
 apply (fun i : natproj2_sigT _ _ (H i)).
Qed.

End Choice.

Section Logical_Remarks.

We prove a few logical results which are helpful to have as lemmas when A, B and C are non trivial.

Lemma CNot_Not_or : A B C : CProp,
 (A~ C) → (B~ C) → ¬ ~ (A or B) → ~ C.
Proof.
 intros A B C H H0 H1.
 intro H2.
 apply H1.
 intro H3.
 elim H3.
  intro; apply H; auto.
 intro; apply H0; auto.
Qed.

Lemma CdeMorgan_ex_all : (A : Type) (P : ACProp) (X : Type),
 (sigT PX) → a : A, P aX.
Proof.
 intros A P X H a H0.
 eauto.
Qed.

End Logical_Remarks.

Section CRelation_Definition.

CProp-valued Relations

Similar to Relations.v in Coq's standard library.
Let A:Type and R:Crelation.

Variable A : Type.

Definition Crelation := AACProp.

Variable R : Crelation.

Definition Creflexive : CProp :=
   x : A, R x x.

Definition Ctransitive : CProp :=
   x y z : A, R x yR y zR x z.

Definition Csymmetric : CProp :=
   x y : A, R x yR y x.

Record Cequivalence : CProp :=
  {Cequiv_refl : Creflexive;
   Cequiv_symm : Csymmetric;
   Cequiv_trans : Ctransitive}.

Definition Cdecidable (P:CProp):= P or ~ P.

End CRelation_Definition.

Fixpoint member (A : Type) (n : A) (l : list A) {struct l} : CProp :=
  match l with
  | nil
  | cons y mmember A n m or y = n
  end.

Implicit Arguments member [A].

Section TRelation_Definition.

Prop-valued Relations

Analogous.
Let A:Type and R:Trelation.

Variable A : Type.

Definition Trelation := AAProp.

Variable R : Trelation.

Definition Treflexive : CProp := x : A, R x x.

Definition Ttransitive : CProp := x y z : A, R x yR y zR x z.

Definition Tsymmetric : CProp := x y : A, R x yR y x.

Definition Tequiv : CProp := Treflexive and Ttransitive and Tsymmetric.

End TRelation_Definition.

Section le_odd.

The relation le, lt, odd and even in CProp


Inductive Cle (n : nat) : natCProp :=
  | Cle_n : Cle n n
  | Cle_S : m : nat, Cle n mCle n (S m).

Theorem Cnat_double_ind : R : natnatCProp,
 ( n : nat, R 0 n) → ( n : nat, R (S n) 0) →
 ( n m : nat, R n mR (S n) (S m)) → n m : nat, R n m.
Proof.
 simple induction n; auto.
 simple induction m; auto.
Qed.

Theorem my_Cle_ind : (n : nat) (P : natCProp),
 P n → ( m : nat, Cle n mP mP (S m)) →
  n0 : nat, Cle n n0P n0.
Proof.
 intros n P.
 generalize (Cle_rect n (fun (n0 : nat) (H : Cle n n0) ⇒ P n0)); intro.
 assumption.
Qed.

Theorem Cle_n_S : n m : nat, Cle n mCle (S n) (S m).
Proof.
 intros n m H.
 pattern m in |- ×.
 apply (my_Cle_ind n).
   apply Cle_n.
  intros.
  apply Cle_S.
  assumption.
 assumption.
Qed.

Lemma toCle : m n : nat, m nCle m n.
Proof.
 intros m.
 induction m as [| m Hrecm].
  simple induction n.
   intro H.
   apply Cle_n.
  intros n0 H H0.
  apply Cle_S.
  apply H.
  apply le_O_n.
 simple induction n.
  intro.
  elimtype .
  inversion H.
 intros n0 H H0.
 generalize (le_S_n _ _ H0); intro H1.
 generalize (Hrecm _ H1); intro H2.
 apply Cle_n_S.
 assumption.
Qed.

Hint Resolve toCle.

Lemma Cle_to : m n : nat, Cle m nm n.
Proof.
 intros m n H.
 elim H.
  apply le_n.
 intros m0 s H0.
 apply le_S.
 assumption.
Qed.

Definition Clt (m n : nat) : CProp := Cle (S m) n.

Lemma toCProp_lt : m n : nat, m < nClt m n.
Proof.
 unfold lt in |- ×.
 unfold Clt in |- ×.
 intros m n H.
 apply toCle.
 assumption.
Qed.

Lemma Clt_to : m n : nat, Clt m nm < n.
Proof.
 unfold lt in |- ×.
 unfold Clt in |- ×.
 intros m n H.
 apply Cle_to.
 assumption.
Qed.

Lemma Cle_le_S_eq : p q : nat, p q{S p q} + {p = q}.
Proof.
 intros p q H.
 elim (gt_eq_gt_dec p q); intro H0.
  elim H0; auto.
 elimtype .
 apply lt_not_le with q p; auto.
Qed.

Lemma Cnat_total_order : m n : nat, m n{m < n} + {n < m}.
Proof.
 intros m n H.
 elim (gt_eq_gt_dec m n).
  intro H0.
  elim H0; intros.
   left; auto.
  elimtype .
  auto.
 auto.
Qed.

Inductive Codd : natCProp :=
    Codd_S : n : nat, Ceven nCodd (S n)
with Ceven : natCProp :=
  | Ceven_O : Ceven 0
  | Ceven_S : n : nat, Codd nCeven (S n).

Lemma Codd_even_to : n : nat, (Codd nodd n) (Ceven neven n).
Proof.
 simple induction n.
  split.
   intro H.
   inversion H.
  intro.
  apply even_O.
 intros n0 H.
 elim H; intros H0 H1.
 split.
  intro H2.
  inversion H2.
  apply odd_S.
  apply H1.
  assumption.
 intro H2.
 inversion H2.
 apply even_S.
 apply H0.
 assumption.
Qed.

Lemma Codd_to : n : nat, Codd nodd n.
Proof.
 intros n H.
 elim (Codd_even_to n); auto.
Qed.

Lemma Ceven_to : n : nat, Ceven neven n.
Proof.
 intros n H.
 elim (Codd_even_to n); auto.
Qed.

Lemma to_Codd_even : n : nat, (odd nCodd n) and (even nCeven n).
Proof.
 simple induction n.
  split.
   intro H.
   elimtype .
   inversion H.
  intro H.
  apply Ceven_O.
 intros n0 H.
 elim H; intros H0 H1.
 split.
  intro H2.
  apply Codd_S.
  apply H1.
  inversion H2.
  assumption.
 intro H2.
 apply Ceven_S.
 apply H0.
 inversion H2.
 assumption.
Qed.

Lemma to_Codd : n : nat, odd nCodd n.
Proof.
 intros.
 elim (to_Codd_even n); auto.
Qed.

Lemma to_Ceven : n : nat, even nCeven n.
Proof.
 intros.
 elim (to_Codd_even n); auto.
Qed.

End le_odd.

Section Misc.

Miscellaneous


Lemma CZ_exh : z : Z, {n : nat | z = n} or {n : nat | z = (- n)%Z}.
Proof.
 intro z.
 elim z.
   left.
    0.
   auto.
  intro p.
  left.
   (nat_of_P p).
  rewrite convert_is_POS.
  reflexivity.
 intro p.
 right.
  (nat_of_P p).
 rewrite min_convert_is_NEG.
 reflexivity.
Qed.

Lemma Cnats_Z_ind : P : ZCProp,
 ( n : nat, P n) → ( n : nat, P (- n)%Z) → z : Z, P z.
Proof.
 intros P H H0 z.
 elim (CZ_exh z); intros H1.
  elim H1; intros n H2.
  rewrite H2.
  apply H.
 elim H1; intros n H2.
 rewrite H2.
 apply H0.
Qed.

Lemma Cdiff_Z_ind : P : ZCProp,
 ( m n : nat, P (m - n)%Z) → z : Z, P z.
Proof.
 intros P H z.
 apply Cnats_Z_ind.
  intro n.
  replace (Z_of_nat n) with (n - 0%nat)%Z.
   apply H.
  simpl in |- ×.
  auto with zarith.
 intro n.
 replace (- n)%Z with (0%nat - n)%Z.
  apply H.
 simpl in |- ×.
 reflexivity.
Qed.

Lemma Cpred_succ_Z_ind : P : ZCProp,
 P 0%Z → ( n : Z, P nP (n + 1)%Z) →
 ( n : Z, P nP (n - 1)%Z) → z : Z, P z.
Proof.
 intros P H H0 H1 z.
 apply Cnats_Z_ind.
  intro n.
  elim n.
   exact H.
  intros n0 H2.
  replace (S n0:Z) with (n0 + 1)%Z.
   apply H0.
   assumption.
  rewrite Znat.inj_S.
  reflexivity.
 intro n.
 elim n.
  exact H.
 intros n0 H2.
 replace (- S n0)%Z with (- n0 - 1)%Z.
  apply H1.
  assumption.
 rewrite Znat.inj_S.
 unfold Zsucc in |- ×.
 rewrite Zopp_plus_distr.
 reflexivity.
Qed.

Lemma not_r_sum_rec : (A B S : Set) (l r : S), ~ B H : A + B,
 sum_rec (fun _ : A + BS) (fun x : Al) (fun x : Br) H = l.
Proof.
 intros A B S l r H H0. elim H0.
 intro a. reflexivity.
  intro b. elim H. assumption.
Qed.

Lemma not_l_sum_rec : (A B S : Set) (l r : S), ~ A H : A + B,
 sum_rec (fun _ : A + BS) (fun x : Al) (fun x : Br) H = r.
Proof.
 intros A B S l r H H0. elim H0.
 intro a. elim H. assumption.
  intros. reflexivity.
Qed.

Let M:Type.

Variable M : Type.

Lemma member_app :
   (x : M) (l k : (list M)),
  ( (member x (app k l))
       ((member x k) or (member x l))).
Proof.
 induction k; firstorder.
Qed.

End Misc.

Results about the natural numbers

We now define a class of predicates on a finite subset of natural numbers that will be important throughout all our work. Essentially, these are simply setoid predicates, but for clarity we will never write them in that form but we will single out the preservation of the setoid equality.

Definition nat_less_n_pred (n : nat) (P : i : nat, i < nCProp) :=
   i j : nat, i = j (H : i < n) (H' : j < n), P i HP j H'.

Definition nat_less_n_pred' (n : nat) (P : i : nat, i nCProp) :=
   i j : nat, i = j (H : i n) (H' : j n), P i HP j H'.

Implicit Arguments nat_less_n_pred [n].
Implicit Arguments nat_less_n_pred' [n].

Section Odd_and_Even.

For our work we will many times need to distinguish cases between even or odd numbers. We begin by proving that this case distinction is decidable. Next, we prove the usual results about sums of even and odd numbers:

Lemma even_plus_n_n : n : nat, even (n + n).
Proof.
 intro n; induction n as [| n Hrecn].
  auto with arith.
 replace (S n + S n) with (S (S (n + n))).
  apply even_S; apply odd_S; apply Hrecn.
 rewrite plus_n_Sm; simpl in |- *; auto.
Qed.

Lemma even_or_odd_plus : k : nat, {j : nat & {k = j + j} + {k = S (j + j)}}.
Proof.
 intro k.
 elim (even_odd_dec k); intro H.
  elim (even_2n k H); intros j Hj; j; auto.
 elim (odd_S2n k H); intros j Hj; j; auto.
Qed.

Finally, we prove that an arbitrary natural number can be written in some canonical way.

Lemma even_or_odd_plus_gt : i j : nat,
 i j{k : nat & {j = i + (k + k)} + {j = i + S (k + k)}}.
Proof.
 intros i j H.
 elim (even_or_odd_plus (j - i)).
 intros k Hk.
 elim Hk; intro H0.
   k; left; rewrite <- H0; auto with arith.
  k; right; rewrite <- H0; auto with arith.
Qed.

End Odd_and_Even.

Hint Resolve even_plus_n_n: arith.
Hint Resolve toCle: core.

Section Natural_Numbers.

Algebraic Properties

We now present a series of trivial things proved with Omega that are stated as lemmas to make proofs shorter and to aid in auxiliary definitions. Giving a name to these results allows us to use them in definitions keeping conciseness.

Lemma Clt_le_weak : i j : nat, Clt i jCle i j.
Proof.
 intros.
 apply toCle; apply lt_le_weak; apply Clt_to; assumption.
Qed.

Lemma lt_5 : i n : nat, i < npred i < n.
Proof.
 intros; apply le_lt_trans with (pred n).
  apply le_pred; auto with arith.
 apply lt_pred_n_n; apply le_lt_trans with i; auto with arith.
Qed.

Lemma lt_8 : m n : nat, m < pred nm < n.
Proof.
 intros; apply lt_le_trans with (pred n); auto with arith.
Qed.

Lemma pred_lt : m n : nat, m < pred nS m < n.
Proof.
 intros; apply le_lt_trans with (pred n); auto with arith.
 apply lt_pred_n_n; apply le_lt_trans with m.
  auto with arith.
 apply lt_le_trans with (pred n); auto with arith.
Qed.

Lemma lt_10 : i m n : nat,
 0 < ii < pred (m + n) → pred i < pred m + pred n.
Proof.
 intros; omega.
Qed.

Lemma lt_pred' : m n : nat, 0 < mm < npred m < pred n.
Proof.
 intros m n H H0; red in |- ×.
 destruct n.
  inversion H0.
 rewrite <- (S_pred m 0); auto.
 simpl in |- ×.
 auto with arith.
Qed.

Lemma le_1 : m n : nat, Cle m npred m n.
Proof.
 intros.
 cut (m n); [ intro | apply Cle_to; assumption ].
 apply le_trans with (pred n); auto with arith.
 apply le_pred; auto.
Qed.

Lemma le_2 : i j : nat, i < ji pred j.
Proof.
 intros; omega.
Qed.

Lemma plus_eq_one_imp_eq_zero : m n : nat,
 m + n 1 → {m = 0} + {n = 0}.
Proof.
 intros m n H.
 elim (le_lt_dec m 0); intro.
  left; auto with arith.
 right; omega.
Qed.

Lemma not_not_lt : i j : nat, ¬ ¬ i < ji < j.
Proof.
 intros; omega.
Qed.

Lemma plus_pred_pred_plus :
   i j k,
  k pred i + pred j
  k pred (i + j).
Proof.
 intros; omega.
Qed.

We now prove some properties of functions on the natural numbers.
Let H:natnat.

Variable h : natnat.

First we characterize monotonicity by a local condition: if h(n) < h(n+1) for every natural number n then h is monotonous. An analogous result holds for weak monotonicity.

Lemma nat_local_mon_imp_mon :
  ( i : nat, h i < h (S i)) →
   i j : nat, i < jh i < h j.
Proof.
 intros H i j H0.
 induction j as [| j Hrecj].
  elimtype ; omega.
 cut (i j); [ intro H1 | auto with arith ].
 elim (le_lt_eq_dec _ _ H1); intro H2.
  cut (h i < h j); [ intro | apply Hrecj; assumption ].
  cut (h j < h (S j)); [ intro | apply H ].
  apply lt_trans with (h j); auto.
 rewrite H2; apply H.
Qed.

Lemma nat_local_mon_imp_mon_le :
  ( i : nat, h i h (S i)) →
   i j : nat, i jh i h j.
Proof.
 intros H i j H0.
 induction j as [| j Hrecj].
  cut (i = 0); [ intro H1 | auto with arith ].
  rewrite H1; apply le_n.
 elim (le_lt_eq_dec _ _ H0); intro H1.
  cut (h i h j); [ intro | apply Hrecj; auto with arith ].
  cut (h j h (S j)); [ intro | apply H ].
  apply le_trans with (h j); auto.
 rewrite H1; apply le_n.
Qed.

A strictly increasing function is injective:

Lemma nat_mon_imp_inj : ( i j : nat, i < jh i < h j) →
  i j : nat, h i = h ji = j.
Proof.
 intros H i j H0.
 cut (¬ i j); [ omega | intro H1 ].
 cut (i < j j < i); [ intro H2 | omega ].
 inversion_clear H2.
  cut (h i < h j); [ rewrite H0; apply lt_irrefl | apply H; assumption ].
 cut (h j < h i); [ rewrite H0; apply lt_irrefl | apply H; assumption ].
Qed.

And (not completely trivial) a function that preserves lt also preserves le.

Lemma nat_mon_imp_mon' : ( i j : nat, i < jh i < h j) →
  i j : nat, i jh i h j.
Proof.
 intros H i j H0.
 elim (le_lt_eq_dec _ _ H0); intro H1.
  apply lt_le_weak; apply H; assumption.
 rewrite H1; apply le_n.
Qed.

The last lemmas in this section state that a monotonous function in the natural numbers completely covers the natural numbers, that is, for every natural number n there is an i such that h(i) n<(n+1) h(i+1). These are useful for integration.

Lemma mon_fun_covers : ( i j, i < jh i < h j) → h 0 = 0 →
  n, {k : nat | S n h k}{i : nat | h i n | S n h (S i)}.
Proof.
 intros H H0 n H1.
 elim H1; intros k Hk.
 induction k as [| k Hreck].
   0.
   rewrite H0; auto with arith.
  cut (h 0 < h 1); [ intro; apply le_trans with (h 0); auto with arith | apply H; apply lt_n_Sn ].
 cut (h k < h (S k)); [ intro H2 | apply H; apply lt_n_Sn ].
 elim (le_lt_dec (S n) (h k)); intro H3.
  elim (Hreck H3); intros i Hi.
   i; assumption.
  k; auto with arith.
Qed.

Lemma weird_mon_covers : n (f : natnat), ( i, f i < nf i < f (S i)) →
 {m : nat | n f m | i, i < mf i < n}.
Proof.
 intros; induction n as [| n Hrecn].
   0.
   auto with arith.
  intros; inversion H0.
 elim Hrecn.
  2: auto.
 intros m Hm Hm'.
 elim (le_lt_eq_dec _ _ Hm); intro.
   m.
   assumption.
  auto with arith.
  (S m).
  apply le_lt_trans with (f m).
   rewrite b; auto with arith.
  apply H.
  rewrite b; apply lt_n_Sn.
 intros.
 elim (le_lt_eq_dec _ _ H0); intro.
  auto with arith.
 cut (i = m); [ intro | auto ].
 rewrite b; rewrite <- H1.
 apply lt_n_Sn.
Qed.

End Natural_Numbers.

Useful for the Fundamental Theorem of Algebra.

Lemma kseq_prop :
   (k : natnat) (n : nat),
  ( i : nat, 1 k i k i n) →
  ( i : nat, k (S i) k i) →
  {j : nat | S j < 2 × n k j = k (S j) k (S j) = k (S (S j))}.
Proof.
 intros k n.
 generalize k; clear k.
 induction n as [| n Hrecn]; intros k H H0.
  elim (H 0); intros H1 H2.
  generalize (le_trans _ _ _ H1 H2); intro H3.
  elimtype .
  inversion H3.
 elim (eq_nat_dec (k 0) (k 2)).
  intro H1.
   0.
  cut (k 0 = k 1).
   intro H2.
   repeat split.
     omega.
    assumption.
   rewrite <- H1.
   auto.
  apply le_antisym.
   rewrite H1.
   apply H0.
  apply H0.
 intro H1.
 elim (Hrecn (fun m : natk (S (S m)))).
   3: intro; apply H0.
  intros m Hm.
   (S (S m)); omega.
 intro i.
 split.
  elim (H (S (S i))); auto.
 elim (lt_eq_lt_dec (k 0) (k 2)); intro H2.
  elim H2; intro H3.
   generalize (H0 0); intro H4.
   generalize (H0 1); intro H5.
   omega.
  tauto.
 generalize (H 0); intro H3.
 elim H3; intros H4 H5.
 generalize (lt_le_trans _ _ _ H2 H5); intro H6.
 cut (k 2 n).
  2: omega.
 intro H7.
 induction i as [| i Hreci].
  assumption.
 apply le_trans with (k (S (S i))); auto.
Qed.

Section Predicates_to_CProp.

Logical Properties

This section contains lemmas that aid in logical reasoning with natural numbers. First, we present some principles of induction, both for CProp- and Prop-valued predicates. We begin by presenting the results for CProp-valued predicates:

Lemma even_induction :
   P : natCProp,
  P 0 →
  ( n, even nP nP (S (S n))) →
   n, even nP n.
Proof.
 intros P H H0 n.
 pattern n in |- *; apply lt_wf_rect.
 clear n.
 intros n H1 H2.
 induction n as [| n Hrecn].
  auto.
 induction n as [| n Hrecn0].
  elimtype ; inversion H2; inversion H4.
 apply H0.
  inversion H2; inversion H4; auto.
 apply H1.
  auto with arith.
 inversion H2; inversion H4; auto.
Qed.

Lemma odd_induction :
   P : natCProp,
  P 1 →
  ( n, odd nP nP (S (S n))) →
   n, odd nP n.
Proof.
 intros P H H0 n; case n.
  intro H1; elimtype ; inversion H1.
 clear n; intros n H1.
 pattern n in |- *; apply even_induction; auto.
  intros n0 H2 H3; auto with arith.
 inversion H1; auto.
Qed.

Lemma four_induction :
   P : natCProp,
  P 0 → P 1 → P 2 → P 3 →
  ( n, P nP (S (S (S (S n))))) →
   n, P n.
Proof.
 intros.
 apply lt_wf_rect.
 intro m.
 case m; auto.
 clear m; intro m.
 case m; auto.
 clear m; intro m.
 case m; auto.
 clear m; intro m.
 case m; auto with arith.
Qed.

Lemma nat_complete_double_induction : P : natnatCProp,
 ( m n, ( m' n', m' < mn' < nP m' n') → P m n) → m n, P m n.
Proof.
 intros P H m.
 pattern m in |- *; apply lt_wf_rect; auto with arith.
Qed.

Lemma odd_double_ind : P : natCProp, ( n, odd nP n) →
 ( n, 0 < nP nP (double n)) → n, 0 < nP n.
Proof.
 cut ( n : nat, 0 < double n → 0 < n). intro.
  intro. intro H0. intro H1. intro n.
  pattern n in |- ×.
  apply lt_wf_rect. intros n0 H2 H3.
  generalize (even_odd_dec n0). intro H4. elim H4.
  intro.
   rewrite (even_double n0).
    apply H1.
     apply H.
     rewrite <- (even_double n0). assumption.
      assumption.
    apply H2.
     apply lt_div2. assumption.
     rewrite (even_double n0) in H3.
     apply H. assumption.
     assumption.
   assumption.
  exact (H0 n0).
 unfold double in |- ×. intros.
 case (zerop n). intro.
  absurd (0 < n + n).
   rewrite e. auto with arith.
   assumption.
 intro. assumption.
Qed.

For subsetoid predicates in the natural numbers we can eliminate disjunction (and existential quantification) as follows.

Lemma finite_or_elim :
   (n : nat) (P Q : i, i nCProp),
  nat_less_n_pred' P
  nat_less_n_pred' Q
  ( i H, P i H or Q i H) →
  {m : nat | {Hm : m n | P m Hm}} or ( i H, Q i H).
Proof.
 intro n; induction n as [| n Hrecn].
  intros P Q HP HQ H.
  elim (H _ (le_n 0)); intro H0.
   left; 0; (le_n 0); assumption.
  right; intros i H1.
  apply HQ with (H := le_n 0); auto with arith.
 intros P Q H H0 H1.
 elim (H1 _ (le_n (S n))); intro H2.
  left; (S n); (le_n (S n)); assumption.
 set (P' := fun (i : nat) (H : i n) ⇒ P i (le_S _ _ H)) in ×.
 set (Q' := fun (i : nat) (H : i n) ⇒ Q i (le_S _ _ H)) in ×.
 cut ({m : nat | {Hm : m n | P' m Hm}} or ( (i : nat) (H : i n), Q' i H)).
  intro H3; elim H3; intro H4.
   left.
   elim H4; intros m Hm; elim Hm; clear H4 Hm; intros Hm Hm'.
    m.
   unfold P' in Hm'.
    (le_S _ _ Hm).
   eapply H with (i := m); [ omega | apply Hm' ].
  right.
  intros i H5.
  unfold Q' in H4.
  elim (le_lt_eq_dec _ _ H5); intro H6.
   cut (i n); [ intro | auto with arith ].
   eapply H0 with (i := i); [ auto with arith | apply (H4 i H7) ].
  eapply H0 with (i := S n); [ auto with arith | apply H2 ].
 apply Hrecn.
   intro i; intros j H3 H4 H5 H6.
   unfold P' in |- ×.
   exact (H _ _ H3 _ _ H6).
  intro i; intros j H3 H4 H5 H6.
  unfold Q' in |- ×.
  exact (H0 _ _ H3 _ _ H6).
 intros i H3.
 unfold P', Q' in |- *; apply H1.
Qed.

Lemma str_finite_or_elim :
   (n : nat) (P Q : i, i nCProp),
  nat_less_n_pred' P
  nat_less_n_pred' Q
  ( i H, P i H or Q i H) →
  {j : nat | {Hj : j n | P j Hj and ( j' Hj', j' < jQ j' Hj')}}
  or ( i H, Q i H).
Proof.
 intro n; induction n as [| n Hrecn].
  intros P Q H H0 H1.
  elim (H1 0 (le_n 0)); intro HPQ.
   left.
    0; (le_n 0).
   split.
    apply H with (H := le_n 0); auto.
   intros; elimtype ; inversion H2.
  right; intros.
  apply H0 with (H := le_n 0); auto with arith.
 intros P Q H H0 H1.
 set (P' := fun (i : nat) (H : i n) ⇒ P i (le_S _ _ H)) in ×.
 set (Q' := fun (i : nat) (H : i n) ⇒ Q i (le_S _ _ H)) in ×.
 elim (Hrecn P' Q').
     intro H2.
     left.
     elim H2; intros m Hm; elim Hm; clear H2 Hm; intros Hm Hm'.
      m.
     unfold P' in Hm'.
      (le_S _ _ Hm).
     elim Hm'; clear Hm'; intros Hm' Hj.
     split.
      eapply H with (i := m); [ auto with arith | apply Hm' ].
     unfold Q' in Hj; intros j' Hj' H2.
     cut (j' n); [ intro H4 | apply le_trans with m; auto with arith ].
     apply H0 with (H := le_S _ _ H4); [ auto | apply Hj; assumption ].
    elim (H1 (S n) (le_n (S n))); intro H1'.
     intro H2.
     left; (S n); (le_n (S n)); split.
      assumption.
     intros j' Hj' H3; unfold Q' in H1'.
     cut (j' n); [ intro H4 | auto with arith ].
     unfold Q' in H2.
     apply H0 with (H := le_S _ _ H4); auto.
    intro H2.
    right; intros i H3.
    unfold Q' in H1'.
    elim (le_lt_eq_dec _ _ H3); intro H4.
     cut (i n); [ intro H5 | auto with arith ].
     unfold Q' in H2.
     apply H0 with (H := le_S _ _ H5); auto.
    apply H0 with (H := le_n (S n)); auto.
   intro i; intros j H2 H3 H4 H5.
   unfold P' in |- ×.
   exact (H _ _ H2 _ _ H5).
  intro i; intros j H2 H3 H4 H5.
  unfold Q' in |- ×.
  exact (H0 _ _ H2 _ _ H5).
 intros i H2.
 unfold P', Q' in |- ×.
 apply H1.
Qed.

End Predicates_to_CProp.

Section Predicates_to_Prop.

Finally, analogous results for Prop-valued predicates are presented for completeness's sake.

Lemma even_ind : P : natProp,
 P 0 → ( n, even nP nP (S (S n))) → n, even nP n.
Proof.
 intros P H H0 n.
 pattern n in |- *; apply lt_wf_ind.
 clear n.
 intros n H1 H2.
 induction n as [| n Hrecn].
  auto.
 induction n as [| n Hrecn0].
  elimtype ; inversion H2; inversion H4.
 apply H0.
  inversion H2; inversion H4; auto.
 apply H1.
  auto with arith.
 inversion H2; inversion H4; auto.
Qed.

Lemma odd_ind : P : natProp,
 P 1 → ( n, P nP (S (S n))) → n, odd nP n.
Proof.
 intros P H H0 n; case n.
  intro H1; elimtype ; inversion H1.
 clear n; intros n H1.
 pattern n in |- *; apply even_ind; auto.
 inversion H1; auto.
Qed.

Lemma nat_complete_double_ind :
   P : natnatProp,
  ( m n, ( m' n', m' < mn' < nP m' n') → P m n) →
   m n, P m n.
Proof.
 intros P H m.
 pattern m in |- *; apply lt_wf_ind; auto.
Qed.

Lemma four_ind :
   P : natProp,
  P 0 → P 1 → P 2 → P 3 →
  ( n, P nP (S (S (S (S n))))) → n, P n.
Proof.
 intros.
 apply lt_wf_ind.
 intro m.
 case m; auto.
 clear m; intro m.
 case m; auto.
 clear m; intro m.
 case m; auto.
 clear m; intro m.
 case m; auto with arith.
Qed.

End Predicates_to_Prop.

Integers

Similar results for integers.


Definition Zlts (x y : Z) := eq (A:=Datatypes.comparison) (x ?= y)%Z Datatypes.Lt.

Lemma toCProp_Zlt : x y : Z, (x < y)%ZZlts x y.
Proof.
 intros x y H.
 unfold Zlts in |- ×.
 unfold Zlt in H.
 auto.
Qed.

Lemma CZlt_to : x y : Z, Zlts x y → (x < y)%Z.
Proof.
 intros x y H.
 unfold Zlt in |- ×.
 inversion H.
 auto.
Qed.

Lemma Zsgn_1 : x : Z, {Zsgn x = 0%Z} + {Zsgn x = 1%Z} + {Zsgn x = (-1)%Z}.
Proof.
 intro x.
 case x.
   left.
   left.
   unfold Zsgn in |- ×.
   reflexivity.
  intro p.
  simpl in |- ×.
  left.
  right.
  reflexivity.
 intro p.
 right.
 simpl in |- ×.
 reflexivity.
Qed.

Lemma Zsgn_2 : x : Z, Zsgn x = 0%Zx = 0%Z.
Proof.
 intro x.
 case x.
   intro H.
   reflexivity.
  intros p H.
  inversion H.
 intros p H.
 inversion H.
Qed.

Lemma Zsgn_3 : x : Z, x 0%ZZsgn x 0%Z.
Proof.
 intro x.
 case x.
   intro H.
   elim H.
   reflexivity.
  intros p H.
  simpl in |- ×.
  discriminate.
 intros p H.
 simpl in |- ×.
 discriminate.
Qed.

The following have unusual names, in line with the series of lemmata in fast_integers.v.

Lemma ZL4' : y : positive, {h : nat | nat_of_P y = S h}.
Proof.
 simple induction y; [ intros p H; elim H; intros x H1; (S x + S x);
   unfold nat_of_P in |- *; simpl in |- *; rewrite ZL0;
     rewrite Pmult_nat_r_plus_morphism; unfold nat_of_P in H1; rewrite H1; auto with arith
       | intros p H1; elim H1; intros x H2; (x + S x);
         unfold nat_of_P in |- *; simpl in |- *; rewrite ZL0;
           rewrite Pmult_nat_r_plus_morphism; unfold nat_of_P in H2; rewrite H2; auto with arith
             | 0; auto with arith ].
Qed.

Lemma ZL9 : p : positive, Z_of_nat (nat_of_P p) = Zpos p.
Proof.
 intro p.
 elim (ZL4 p).
 intros x H0.
 rewrite H0.
 unfold Z_of_nat in |- ×.
 apply f_equal with (A := positive) (B := Z) (f := Zpos).
 cut (P_of_succ_nat (nat_of_P p) = P_of_succ_nat (S x)).
  intro H1.
  rewrite P_of_succ_nat_o_nat_of_P_eq_succ in H1.
  cut (Ppred (Psucc p) = Ppred (P_of_succ_nat (S x))).
   intro H2.
   rewrite Ppred_succ in H2.
   simpl in H2.
   rewrite Ppred_succ in H2.
   auto.
  apply f_equal with (A := positive) (B := positive) (f := Ppred).
  assumption.
 apply f_equal with (f := P_of_succ_nat).
 assumption.
Qed.

Theorem Zsgn_4 : a : Z, a = (Zsgn a × Zabs_nat a)%Z.
Proof.
 intro a.
 case a.
   simpl in |- ×.
   reflexivity.
  intro p.
  unfold Zsgn in |- ×.
  unfold Zabs_nat in |- ×.
  rewrite Zmult_1_l.
  symmetry in |- ×.
  apply ZL9.
 intro p.
 unfold Zsgn in |- ×.
 unfold Zabs_nat in |- ×.
 rewrite ZL9.
 constructor.
Qed.

Theorem Zsgn_5 : a b x y : Z, x 0%Zy 0%Z
 (Zsgn a × x)%Z = (Zsgn b × y)%Z → (Zsgn a × y)%Z = (Zsgn b × x)%Z.
Proof.
 intros a b x y H H0.
 case a.
   case b.
     simpl in |- ×.
     trivial.
    intro p.
    unfold Zsgn in |- ×.
    intro H1.
    rewrite Zmult_1_l in H1.
    simpl in H1.
    elim H0.
    auto.
   intro p.
   unfold Zsgn in |- ×.
   intro H1.
   elim H0.
   apply Zopp_inj.
   simpl in |- ×.
   transitivity (-1 × y)%Z; auto.
  intro p.
  unfold Zsgn at 1 in |- ×.
  unfold Zsgn at 2 in |- ×.
  intro H1.
  transitivity y.
   rewrite Zmult_1_l.
   reflexivity.
  transitivity (Zsgn b × (Zsgn b × y))%Z.
   case (Zsgn_1 b).
    intro H2.
    case H2.
     intro H3.
     elim H.
     rewrite H3 in H1.
     change ((1 × x)%Z = 0%Z) in H1.
     rewrite Zmult_1_l in H1.
     assumption.
    intro H3.
    rewrite H3.
    rewrite Zmult_1_l.
    rewrite Zmult_1_l.
    reflexivity.
   intro H2.
   rewrite H2.
   ring.
  rewrite Zmult_1_l in H1.
  rewrite H1.
  reflexivity.
 intro p.
 unfold Zsgn at 1 in |- ×.
 unfold Zsgn at 2 in |- ×.
 intro H1.
 transitivity (Zsgn b × (-1 × (Zsgn b × y)))%Z.
  case (Zsgn_1 b).
   intro H2.
   case H2.
    intro H3.
    elim H.
    apply Zopp_inj.
    transitivity (-1 × x)%Z.
     ring.
    unfold Zopp in |- ×.
    rewrite H3 in H1.
    transitivity (0 × y)%Z; auto.
   intro H3.
   rewrite H3.
   ring.
  intro H2.
  rewrite H2.
  ring.
 rewrite <- H1.
 ring.
Qed.

Lemma nat_nat_pos : m n : nat, ((m + 1) × (n + 1) > 0)%Z.
Proof.
 intros m n.
 apply Zlt_gt.
 cut (Z_of_nat m + 1 > 0)%Z.
  intro H.
  cut (0 < Z_of_nat n + 1)%Z.
   intro H0.
   cut ((Z_of_nat m + 1) × 0 < (Z_of_nat m + 1) × (Z_of_nat n + 1))%Z.
    rewrite Zmult_0_r.
    auto.
   apply Zlt_reg_mult_l; auto.
  change (0 < Zsucc (Z_of_nat n))%Z in |- ×.
  apply Zle_lt_succ.
  change (Z_of_nat 0 Z_of_nat n)%Z in |- ×.
  apply Znat.inj_le.
  apply le_O_n.
 apply Zlt_gt.
 change (0 < Zsucc (Z_of_nat m))%Z in |- ×.
 apply Zle_lt_succ.
 change (Z_of_nat 0 Z_of_nat m)%Z in |- ×.
 apply Znat.inj_le.
 apply le_O_n.
Qed.

Theorem S_predn : m : nat, m 0 → S (pred m) = m.
Proof.
 intros m H.
 symmetry in |- ×.
 apply S_pred with 0.
 omega.
Qed.

Lemma absolu_1 : x : Z, Zabs_nat x = 0 → x = 0%Z.
Proof.
 intros x H.
 case (dec_eq x 0).
  auto.
 intro H0.
 apply False_ind.
 ElimCompare x 0%Z.
   intro H2.
   apply H0.
   elim (Zcompare_Eq_iff_eq x 0%nat).
   intros H3 H4.
   auto.
  intro H2.
  cut ( h : nat, Zabs_nat x = S h).
   intro H3.
   case H3.
   rewrite H.
   exact O_S.
  change (x < 0)%Z in H2.
  set (H3 := Zlt_gt _ _ H2) in ×.
  elim (Zcompare_Gt_spec _ _ H3).
  intros x0 H5.
  cut ( q : positive, x = Zneg q).
   intro H6.
   case H6.
   intros x1 H7.
   rewrite H7.
   unfold Zabs_nat in |- ×.
   generalize x1.
   exact ZL4.
  cut (x = (- Zpos x0)%Z).
   simpl in |- ×.
   intro H6.
    x0.
   assumption.
  rewrite <- (Zopp_involutive x).
  exact (f_equal Zopp H5).
 intro H2.
 cut ( h : nat, Zabs_nat x = S h).
  intro H3.
  case H3.
  rewrite H.
  exact O_S.
 elim (Zcompare_Gt_spec _ _ H2).
 simpl in |- ×.
 rewrite Zplus_0_r.
 intros x0 H4.
 rewrite H4.
 unfold Zabs_nat in |- ×.
 generalize x0.
 exact ZL4.
Qed.

Lemma absolu_2 : x : Z, x 0%ZZabs_nat x 0.
Proof.
 intros x H.
 intro H0.
 apply H.
 apply absolu_1.
 assumption.
Qed.

Lemma Zgt_mult_conv_absorb_l : a x y : Z,
 (a < 0)%Z → (a × x > a × y)%Z → (x < y)%Z.
Proof.
 intros a x y H H0.
 case (dec_eq x y).
  intro H1.
  apply False_ind.
  rewrite H1 in H0.
  cut ((a × y)%Z = (a × y)%Z).
   change ((a × y)%Z (a × y)%Z) in |- ×.
   apply Zgt_not_eq.
   assumption.
  trivial.
 intro H1.
 case (not_Zeq x y H1).
  trivial.
 intro H2.
 apply False_ind.
 cut (a × y > a × x)%Z.
  apply Zgt_asym with (m := (a × y)%Z) (n := (a × x)%Z).
  assumption.
 apply Zlt_conv_mult_l.
  assumption.
 assumption.
Qed.

Lemma Zgt_mult_reg_absorb_l : a x y : Z,
 (a > 0)%Z → (a × x > a × y)%Z → (x > y)%Z.
Proof.
 intros a x y H H0.
 cut (- a < - (0))%Z.
  rewrite <- (Zopp_involutive a) in H.
  rewrite <- (Zopp_involutive 0) in H.
  simpl in |- ×.
  intro H1.
  rewrite <- (Zopp_involutive x).
  rewrite <- (Zopp_involutive y).
  apply Zlt_opp.
  apply Zgt_mult_conv_absorb_l with (a := (- a)%Z) (x := (- x)%Z).
   assumption.
  rewrite Zopp_mult_distr_l_reverse.
  rewrite Zopp_mult_distr_l_reverse.
  apply Zlt_opp.
  rewrite <- Zopp_mult_distr_r.
  rewrite <- Zopp_mult_distr_r.
  apply Zgt_lt.
  apply Zlt_opp.
  apply Zgt_lt.
  assumption.
 omega.
Qed.

Lemma Zmult_Sm_Sn : m n : Z,
 ((m + 1) × (n + 1))%Z = (m × n + (m + n) + 1)%Z.
Proof.
 intros.
 ring.
Qed.

Definition CForall {A: Type} (P: AType): list AType :=
  fold_right (fun xprod (P x)) True.

Definition CForall_prop {A: Type} (P: AProp) (l: list A):
 ( x, In x lP x) IFF CForall P l.
Proof with firstorder. induction l... subst... Qed.

Lemma CForall_indexed {A} (P: AType) (l: list A): CForall P l
   i (d: A), (i < length l)%natP (nth i l d).
Proof.
 intros X i.
 revert l X.
 induction i; destruct l; simpl in *; intuition; exfalso; inversion H.
Qed.

Lemma CForall_map {A B} (P: BType) (f: AB) (l: list A):
  CForall P (map f l) IFF CForall (fun xP (f x)) l.
Proof. induction l; firstorder. Qed.

Lemma CForall_weak {A} (P Q: AType):
  ( x, P xQ x) →
  ( l, CForall P lCForall Q l).
Proof. induction l; firstorder. Qed.

Fixpoint CNoDup {T: Type} (R: TTType) (l: list T): Type :=
  match l with
  | nilTrue
  | h :: tprod (CNoDup R t) (CForall (R h) t)
  end.

Lemma CNoDup_weak {A: Type} (Ra Rb: AAType) (l: list A):
  ( x y, Ra x yRb x y) →
  CNoDup Ra lCNoDup Rb l.
Proof with auto.
 induction l... firstorder.
 apply CForall_weak with (Ra a)...
Qed.

Lemma CNoDup_indexed {T} (R: TTType) (Rsym: Csymmetric _ R) (l: list T) (d: T): CNoDup R l
   i j, (i < length l)%nat → (j < length l)%nati jR (nth i l d) (nth j l d).
Proof with intuition.
 induction l; simpl...
  exfalso...
 destruct i.
  destruct j...
  apply (CForall_indexed (R a) l)...
 destruct j...
 apply Rsym.
 apply (CForall_indexed (R a) l)...
Qed.

Lemma CNoDup_map {A B: Type} (R: BBType) (f: AB):
   l, CNoDup (fun x yR (f x) (f y)) l IFF CNoDup R (map f l).
Proof with auto; intuition.
 induction l; simpl...
 split; intro; split.
    apply IHl, X.
   apply CForall_map...
  apply IHl, X.
 apply CForall_map...
Qed.