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 s1->s2->s3, 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.
Basics
Here we treat conversion from Prop to CProp and vice versa, and some basic connectives in CProp.Definition ~ (P : CProp) := P -> ⊥.
Inductive CAnd (A B : CProp) : CProp := CAnd_intro : A -> B -> CAnd A B.
Lemma CAnd_proj1 : forall A B : CProp, (CAnd A B) -> A.
Lemma CAnd_proj2 : forall A B : CProp, (CAnd A B) -> B.
Definition ⇔ (A B : CProp) : CProp := CAnd (A -> B) (B -> A).
Inductive ⊥ : CProp :=.
Inductive CTrue : CProp := CI : CTrue.
Inductive sumT (A B : Type) : Type :=
| inlT : A -> sumT A B
| inrT : B -> sumT A B.
Definition proj1_sigT (A : Type) (P : A -> CProp) (e : sigT P) :=
match e with
| existT a b => a
end.
Definition proj2_sigT (A : Type) (P : A -> CProp) (e : sigT P) :=
match e return (P (proj1_sigT A P e)) with
| existT a b => b
end.
Inductive sig2T (A : Type) (P Q : A -> CProp) : CProp :=
exist2T : forall x : A, P x -> Q x -> sig2T A P Q.
Definition proj1_sig2T (A : Type) (P Q : A -> CProp) (e : sig2T A P Q) :=
match e with
| exist2T a b c => a
end.
Definition proj2a_sig2T (A : Type) (P Q : A -> CProp) (e : sig2T A P Q) :=
match e return (P (proj1_sig2T A P Q e)) with
| exist2T a b c => b
end.
Definition proj2b_sig2T (A : Type) (P Q : A -> CProp) (e : sig2T A P Q) :=
match e return (Q (proj1_sig2T A P Q e)) with
| exist2T a b c => c
end.
Inductive toCProp (A : Prop) : CProp := ts : A -> toCProp A.
Lemma toCProp_e : forall A : Prop, toCProp A -> forall P : Prop, (A -> P) -> P.
Definition ~ (A : Prop): CProp := A -> ⊥.
Lemma Ccontrapos' : forall A φ : Prop, (A -> φ) -> ~ φ -> ~ A.
Inductive COr (A B : CProp) : CProp :=
| Cinleft : A -> COr A B
| Cinright : B -> COr A B.
End Basics.
Some lemmas to make it possible to use Step when reasoning with bi-implications.
Lemma Iff_left :
forall (A B C : CProp),
(A IFF B) -> (A IFF C) -> (C IFF B).
Lemma Iff_right:
forall (A B C : CProp),
(A IFF B) -> (A IFF C) -> (B IFF C).
Lemma Iff_refl : forall (A : CProp), (A IFF A).
Lemma Iff_sym :
forall (A B : CProp),(A IFF B) -> (B IFF A).
Lemma Iff_trans :
forall (A B C : CProp),
(CAnd (A IFF B) (B IFF C)) -> (A IFF C).
Lemma Iff_imp_imp :
forall (A B : CProp),
(A IFF B) -> (CAnd (A->B) (B->A)).
Lemma not_r_cor_rect :
forall (A B : CProp) (S : Type) (l r : S),
~ B ->
forall H : A or B,
COr_rect A B (fun _ : A or B => S) (fun x : A => l) (fun x : B => r) H = l.
Lemma not_l_cor_rect :
forall (A B : CProp) (S : Type) (l r : S),
~ A ->
forall H : A or B,
COr_rect A B (fun _ : A or B => S) (fun x : A => l) (fun x : B => r) H = r.
Section Choice.
Variable P : N -> N -> Prop.
Lemma choice :
(forall n : N, {m : N | P n m}) ->
{d : N -> N | forall n : N, P n (d n)}.
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 : forall A B C : CProp,
(A -> ~ C) -> (B -> ~ C) -> ~ ~ (A or B) -> ~ C.
Lemma CdeMorgan_ex_all : forall (A : Type) (P : A -> CProp) (X : Type),
(sigT P -> X) -> forall a : A, P a -> X.
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 := A -> A -> CProp.
Variable R : Crelation.
Definition Creflexive : CProp :=
forall x : A, R x x.
Definition Ctransitive : CProp :=
forall x y z : A, R x y -> R y z -> R x z.
Definition Csymmetric : CProp :=
forall x y : A, R x y -> R 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 m => member A n m or y = n
end.
Section TRelation_Definition.
Variable A : Type.
Definition Trelation := A -> A -> Prop.
Variable R : Trelation.
Definition Treflexive : CProp := forall x : A, R x x.
Definition Ttransitive : CProp := forall x y z : A, R x y -> R y z -> R x z.
Definition Tsymmetric : CProp := forall x y : A, R x y -> R y x.
Definition Tequiv : CProp := Treflexive and Ttransitive and Tsymmetric.
End TRelation_Definition.
Section le_odd.
Inductive Cle (n : N) : N -> CProp :=
| Cle_n : Cle n n
| Cle_S : forall m : N, Cle n m -> Cle n (S m).
Theorem Cnat_double_ind : forall R : N -> N -> CProp,
(forall n : N, R 0 n) -> (forall n : N, R (S n) 0) ->
(forall n m : N, R n m -> R (S n) (S m)) -> forall n m : N, R n m.
Theorem my_Cle_ind : forall (n : N) (P : N -> CProp),
P n -> (forall m : N, Cle n m -> P m -> P (S m)) ->
forall n0 : N, Cle n n0 -> P n0.
Theorem Cle_n_S : forall n m : N, Cle n m -> Cle (S n) (S m).
Lemma toCle : forall m n : N, m <= n -> Cle m n.
Lemma Cle_to : forall m n : N, Cle m n -> m <= n.
Definition Clt (m n : N) : CProp := Cle (S m) n.
Lemma toCProp_lt : forall m n : N, m < n -> Clt m n.
Lemma Clt_to : forall m n : N, Clt m n -> m < n.
Lemma Cle_le_S_eq : forall p q : N, p <= q -> {S p <= q} + {p = q}.
Lemma Cnat_total_order : forall m n : N, m <> n -> {m < n} + {n < m}.
Inductive Codd : N -> CProp :=
Codd_S : forall n : N, Ceven n -> Codd (S n)
with Ceven : N -> CProp :=
| Ceven_O : Ceven 0
| Ceven_S : forall n : N, Codd n -> Ceven (S n).
Lemma Codd_even_to : forall n : N, (Codd n -> odd n) /\ (Ceven n -> even n).
Lemma Codd_to : forall n : N, Codd n -> odd n.
Lemma Ceven_to : forall n : N, Ceven n -> even n.
Lemma to_Codd_even : forall n : N, (odd n -> Codd n) and (even n -> Ceven n).
Lemma to_Codd : forall n : N, odd n -> Codd n.
Lemma to_Ceven : forall n : N, even n -> Ceven n.
End le_odd.
Section Misc.
Lemma CZ_exh : forall z : Z, {n : N | z = n} or {n : N | z = (- n)%Z}.
Lemma Cnats_Z_ind : forall P : Z -> CProp,
(forall n : N, P n) -> (forall n : N, P (- n)%Z) -> forall z : Z, P z.
Lemma Cdiff_Z_ind : forall P : Z -> CProp,
(forall m n : N, P (m - n)%Z) -> forall z : Z, P z.
Lemma Cpred_succ_Z_ind : forall P : Z -> CProp,
P 0%Z -> (forall n : Z, P n -> P (n + 1)%Z) ->
(forall n : Z, P n -> P (n - 1)%Z) -> forall z : Z, P z.
Lemma not_r_sum_rec : forall (A B S : Set) (l r : S), ~ B -> forall H : A + B,
sum_rec (fun _ : A + B => S) (fun x : A => l) (fun x : B => r) H = l.
Lemma not_l_sum_rec : forall (A B S : Set) (l r : S), ~ A -> forall H : A + B,
sum_rec (fun _ : A + B => S) (fun x : A => l) (fun x : B => r) H = r.
Let M:Type.
Variable M : Type.
Lemma member_app :
forall (x : M) (l k : (list M)),
(⇔ (member x (app k l))
((member x k) or (member x l))).
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 : N) (P : forall i : N, i < n -> CProp) :=
forall i j : N, i = j -> forall (H : i < n) (H' : j < n), P i H -> P j H'.
Definition nat_less_n_pred' (n : N) (P : forall i : N, i <= n -> CProp) :=
forall i j : N, i = j -> forall (H : i <= n) (H' : j <= n), P i H -> P j H'.
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 : forall n : N, even (n + n).
Lemma even_or_odd_plus : forall k : N, {j : N & {k = j + j} + {k = S (j + j)}}.
Finally, we prove that an arbitrary natural number can be written in some canonical way.
Lemma even_or_odd_plus_gt : forall i j : N,
i <= j -> {k : N & {j = i + (k + k)} + {j = i + S (k + k)}}.
End Odd_and_Even.
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 : forall i j : N, Clt i j -> Cle i j.
Lemma lt_5 : forall i n : N, i < n -> pred i < n.
Lemma lt_8 : forall m n : N, m < pred n -> m < n.
Lemma pred_lt : forall m n : N, m < pred n -> S m < n.
Lemma lt_10 : forall i m n : N,
0 < i -> i < pred (m + n) -> pred i < pred m + pred n.
Lemma lt_pred' : forall m n : N, 0 < m -> m < n -> pred m < pred n.
Lemma le_1 : forall m n : N, Cle m n -> pred m <= n.
Lemma le_2 : forall i j : N, i < j -> i <= pred j.
Lemma plus_eq_one_imp_eq_zero : forall m n : N,
m + n <= 1 -> {m = 0} + {n = 0}.
Lemma not_not_lt : forall i j : N, ~ ~ i < j -> i < j.
Lemma plus_pred_pred_plus :
forall i j k,
k <= pred i + pred j ->
k <= pred (i + j).
We now prove some properties of functions on the natural numbers.
Let H:nat->nat.
Let H:nat->nat.
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 :
(forall i : N, h i < h (S i)) ->
forall i j : N, i < j -> h i < h j.
Lemma nat_local_mon_imp_mon_le :
(forall i : N, h i <= h (S i)) ->
forall i j : N, i <= j -> h i <= h j.
A strictly increasing function is injective:
And (not completely trivial) a function that preserves lt also preserves le.
Lemma nat_mon_imp_mon' : (forall i j : N, i < j -> h i < h j) ->
forall i j : N, i <= j -> h i <= h j.
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 : (forall i j, i < j -> h i < h j) -> h 0 = 0 ->
forall n, {k : N | S n <= h k} -> {i : N | h i <= n | S n <= h (S i)}.
Lemma weird_mon_covers : forall n (f : N -> N), (forall i, f i < n -> f i < f (S i)) ->
{m : N | n <= f m | forall i, i < m -> f i < n}.
End Natural_Numbers.
Useful for the Fundamental Theorem of Algebra.
Lemma kseq_prop :
forall (k : N -> N) (n : N),
(forall i : N, 1 <= k i /\ k i <= n) ->
(forall i : N, k (S i) <= k i) ->
{j : N | S j < 2 * n /\ k j = k (S j) /\ k (S j) = k (S (S j))}.
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 :
forall P : N -> CProp,
P 0 ->
(forall n, even n -> P n -> P (S (S n))) ->
forall n, even n -> P n.
Lemma odd_induction :
forall P : N -> CProp,
P 1 ->
(forall n, odd n -> P n -> P (S (S n))) ->
forall n, odd n -> P n.
Lemma four_induction :
forall P : N -> CProp,
P 0 -> P 1 -> P 2 -> P 3 ->
(forall n, P n -> P (S (S (S (S n))))) ->
forall n, P n.
Lemma nat_complete_double_induction : forall P : N -> N -> CProp,
(forall m n, (forall m' n', m' < m -> n' < n -> P m' n') -> P m n) -> forall m n, P m n.
Lemma odd_double_ind : forall P : N -> CProp, (forall n, odd n -> P n) ->
(forall n, 0 < n -> P n -> P (double n)) -> forall n, 0 < n -> P n.
For subsetoid predicates in the natural numbers we can eliminate
disjunction (and existential quantification) as follows.
Lemma finite_or_elim :
forall (n : N) (P Q : forall i, i <= n -> CProp),
nat_less_n_pred' P ->
nat_less_n_pred' Q ->
(forall i H, P i H or Q i H) ->
{m : N | {Hm : m <= n | P m Hm}} or (forall i H, Q i H).
Lemma str_finite_or_elim :
forall (n : N) (P Q : forall i, i <= n -> CProp),
nat_less_n_pred' P ->
nat_less_n_pred' Q ->
(forall i H, P i H or Q i H) ->
{j : N | {Hj : j <= n | P j Hj and (forall j' Hj', j' < j -> Q j' Hj')}}
or (forall i H, Q i H).
End Predicates_to_CProp.
Section Predicates_to_Prop.
Finally, analogous results for Prop-valued predicates are presented for
completeness's sake.
Lemma even_ind : forall P : N -> Prop,
P 0 -> (forall n, even n -> P n -> P (S (S n))) -> forall n, even n -> P n.
Lemma odd_ind : forall P : N -> Prop,
P 1 -> (forall n, P n -> P (S (S n))) -> forall n, odd n -> P n.
Lemma nat_complete_double_ind :
forall P : N -> N -> Prop,
(forall m n, (forall m' n', m' < m -> n' < n -> P m' n') -> P m n) ->
forall m n, P m n.
Lemma four_ind :
forall P : N -> Prop,
P 0 -> P 1 -> P 2 -> P 3 ->
(forall n, P n -> P (S (S (S (S n))))) -> forall n, P n.
End Predicates_to_Prop.
Definition Zlts (x y : Z) := eq (A:=Datatypes.comparison) (x ?= y)%Z Datatypes.Lt.
Lemma toCProp_Zlt : forall x y : Z, (x < y)%Z -> Zlts x y.
Lemma CZlt_to : forall x y : Z, Zlts x y -> (x < y)%Z.
Lemma Zsgn_1 : forall x : Z, {Zsgn x = 0%Z} + {Zsgn x = 1%Z} + {Zsgn x = (-1)%Z}.
Lemma Zsgn_2 : forall x : Z, Zsgn x = 0%Z -> x = 0%Z.
Lemma Zsgn_3 : forall x : Z, x <> 0%Z -> Zsgn x <> 0%Z.
The following have unusual names, in line with the series of lemmata in
fast_integers.v.
Lemma ZL4' : forall y : positive, {h : N | nat_of_P y = S h}.
Lemma ZL9 : forall p : positive, Z_of_nat (nat_of_P p) = Zpos p.
Theorem Zsgn_4 : forall a : Z, a = (Zsgn a * Zabs_nat a)%Z.
Theorem Zsgn_5 : forall a b x y : Z, x <> 0%Z -> y <> 0%Z ->
(Zsgn a * x)%Z = (Zsgn b * y)%Z -> (Zsgn a * y)%Z = (Zsgn b * x)%Z.
Lemma nat_nat_pos : forall m n : N, ((m + 1) * (n + 1) > 0)%Z.
Theorem S_predn : forall m : N, m <> 0 -> S (pred m) = m.
Lemma absolu_1 : forall x : Z, Zabs_nat x = 0 -> x = 0%Z.
Lemma absolu_2 : forall x : Z, x <> 0%Z -> Zabs_nat x <> 0.
Lemma Zgt_mult_conv_absorb_l : forall a x y : Z,
(a < 0)%Z -> (a * x > a * y)%Z -> (x < y)%Z.
Lemma Zgt_mult_reg_absorb_l : forall a x y : Z,
(a > 0)%Z -> (a * x > a * y)%Z -> (x > y)%Z.
Lemma Zmult_Sm_Sn : forall m n : Z,
((m + 1) * (n + 1))%Z = (m * n + (m + n) + 1)%Z.