Set Implicit Arguments.
Require Import Omega.
Require Import Coq.Init.Nat.
Require Export FinTypes.External.
Require Export FinTypes.FinTypes.
Require Import Omega.
Require Import Coq.Init.Nat.
Require Export FinTypes.External.
Require Export FinTypes.FinTypes.
Utilities
- Tactics for dec and omega
- Basic logical reasoning with propositions satisfying XM (e.g. de Morgan rules)
- Additional dec instances
- Variants of constructive choice
- Strictly monotone functions
- Decidability of bounded quantifiers over nat
- Predicates as languages
Ltac rewrite_eq Eq := let E := fresh in assert (Eq) as E by omega; rewrite E; clear E.
Ltac rewrite_eq_in Eq T := let E := fresh in assert (Eq) as E by omega; rewrite E in T; clear E.
Ltac rewrite_eq_at Eq P := let E := fresh in assert (Eq) as E by omega; rewrite E at P; clear E.
Tactic Notation "rewrite_eq" constr(Eq) := (rewrite_eq Eq).
Tactic Notation "rewrite_eq" constr(Eq) "in" hyp(T) := (rewrite_eq_in Eq T).
Tactic Notation "rewrite_eq" constr(Eq) "at" integer(T) := (rewrite_eq_at Eq T).
We will frequently use omega and hence use it for auto.
Hint Extern 10 (_ = _) => omega.
Hint Extern 10 (_ < _) => omega.
Hint Extern 10 (_ <= _) => omega.
Hint Extern 10 (False) => omega.
Small variants of omega and auto. Only rarely used and possibly could be removed.
Ltac oauto := try (omega); try (cbn;omega); auto.
Ltac comega := cbn; omega.
Ltac comega := cbn; omega.
Tactics for Simplification of Decisions
Lemma decision_true (X:Type) (P:Prop) (decP:dec P) (x y : X) (p:P): (if (decision P) then x else y) = x.
Proof.
decide P.
- reflexivity.
- exfalso. auto.
Qed.
Lemma decision_false (X:Type) (P:Prop) (decP:dec P) (x y : X) (p:~P): (if (decision P) then x else y) = y.
Proof.
decide P.
- exfalso. auto.
- reflexivity.
Qed.
Ltac trivial_decision := repeat ( try (rewrite decision_true in * by auto);
try (rewrite decision_false in * by auto);
try (rewrite decision_true in * by comega);
try (rewrite decision_false in * by comega);
try (rewrite decision_true in * by congruence);
try (rewrite decision_false in * by congruence)).
Proof.
decide P.
- reflexivity.
- exfalso. auto.
Qed.
Lemma decision_false (X:Type) (P:Prop) (decP:dec P) (x y : X) (p:~P): (if (decision P) then x else y) = y.
Proof.
decide P.
- exfalso. auto.
- reflexivity.
Qed.
Ltac trivial_decision := repeat ( try (rewrite decision_true in * by auto);
try (rewrite decision_false in * by auto);
try (rewrite decision_true in * by comega);
try (rewrite decision_false in * by comega);
try (rewrite decision_true in * by congruence);
try (rewrite decision_false in * by congruence)).
Propositions Satisfing XM
We register sat_xm as a typeclass to automatically derive it for some propositions.Definition sat_xm (p : Prop) := p \/ ~ p.
Existing Class sat_xm.
Instance sat_xm_and P Q: sat_xm P -> sat_xm Q -> sat_xm (P /\ Q).
Proof. firstorder. Qed.
Instance sat_xm_or P Q : sat_xm P -> sat_xm Q -> sat_xm (P \/ Q).
Proof. firstorder. Qed.
Instance sat_xm_not P: sat_xm P -> sat_xm (~P).
Proof. firstorder. Qed.
Instance sat_xm_from_dec P: dec P -> sat_xm P.
Proof. firstorder. Qed.
Instance sat_xm_proper : Proper (iff ==> iff) sat_xm.
Proof. firstorder. Qed.
Lemmas for basic logical reasioning. All are provable with firstorder or tauto
but sometimes it is helful to use them explicitly.
Lemma deMorgan_all (X: Type) (P: X -> Prop) : (~ exists x, P x) <-> (forall x, ~ P x).
Proof. firstorder. Qed.
Lemma deMorgan_all_neg (X: Type) (P: X -> Prop) : (forall x, sat_xm (P x)) -> (~ exists x, ~ P x) -> (forall x, P x).
Proof. firstorder. Qed.
Lemma deMorgan_exists (X: Type) (P: X -> Prop) : sat_xm (exists x, P x) -> (~ forall x, ~P x) <-> (exists x, P x).
Proof. firstorder. Qed.
Lemma deMorgan_or (P Q: Prop): sat_xm P -> sat_xm Q -> (~ (~P \/ ~Q)) <-> P /\ Q.
Proof. firstorder. Qed.
Lemma deMorgan_and (P Q: Prop): sat_xm P -> sat_xm Q -> (~ (~P /\ ~Q)) <-> P \/ Q.
Proof. firstorder. Qed.
Lemma deMorgan_and' (P Q: Prop): sat_xm P -> sat_xm Q -> (~ (P /\ Q)) <-> ~P \/ ~Q.
Proof. firstorder. Qed.
Lemma sat_xm_iff (P Q : Prop): P <-> Q -> sat_xm P -> sat_xm Q.
Proof. firstorder. Qed.
Lemma double_negation (P: Prop) : sat_xm P -> P <-> ~~ P.
Proof. firstorder. Qed.
Lemma iff_neg (P Q : Prop) : (P <-> Q) -> (~ P <-> ~ Q) .
Proof. tauto. Qed.
Lemma iff_impl (P1 P2 Q1 Q2 : Prop) : (P1 <-> P2) -> (Q1 <-> Q2) -> ( (P1 -> Q1) <-> (P2 -> Q2)) .
Proof. tauto. Qed.
Lemma iff_impl_true (P : Prop) : (True -> P) <-> P.
Proof. tauto. Qed.
Lemma iff_all (X: Type) (P Q : X -> Prop) : (forall x, P x <-> Q x) -> ((forall x, P x) <-> forall x, Q x).
Proof. firstorder. Qed.
Lemma iff_ex (X: Type) (P Q : X -> Prop) : (forall x, P x <-> Q x) -> ((exists x, P x) <-> exists x, Q x).
Proof. firstorder. Qed.
Lemma bounded_pred (P : nat -> Prop) i k: ( i< k \/ ~P i ) <-> ~(k<= i /\ P i).
Proof.
split.
- intros [H | H] [H2 H3]; auto.
- intros H. decide (i < k); auto.
Qed.
Inductive safe (p : nat -> Prop) (n : nat) : Prop :=
| safeB : p n -> safe p n
| safeS : safe p (S n) -> ~ p n -> safe p n.
Section First.
Variable p : nat -> Prop.
Variable p_dec : forall n, dec (p n).
Lemma safe_dclosed k n : k <= n -> safe p n -> safe p k.
Proof.
intros A B. induction A as [|n A].
- exact B.
- decide (p n); apply IHA.
+ now left.
+ right; auto.
Qed.
Fixpoint first (n : nat) (A : safe p n) : {x | p x /\ forall j, n <= j < x -> ~ p j}.
Proof.
decide (p n).
- exists n. split; auto.
- enough {x : nat | p x /\ (forall j : nat, S n <= j < x -> ~ p j)} as [x [P Q]].
+ exists x. split; auto. intros j B. decide (j = n).
* now subst n.
* apply Q. omega.
+ apply first. destruct A; tauto.
Qed.
Lemma cc_nat_first : (exists x, p x) -> {x | p x /\ forall j, 0 <= j < x -> ~ p j}.
Proof.
intros A. apply first with (n:=0).
destruct A as [n A].
apply safe_dclosed with (n:=n). omega. left. exact A.
Qed.
Lemma cc_nat : (exists x, p x) -> {x | p x}.
Proof.
intros A. destruct (cc_nat_first A) as [x [P _]]. now exists x.
Qed.
Lemma cc_nat_first_extensional (H1 H2: exists x, p x) : proj1_sig (cc_nat_first H1) = proj1_sig (cc_nat_first H2).
Proof.
destruct cc_nat_first as [x [Q1 Q2]].
destruct cc_nat_first as [y [Q3 Q4]]. simpl.
decide (x < y).
- exfalso. apply (Q4 x); oauto.
- decide (y < x); oauto.
exfalso. apply (Q2 y); oauto.
Qed.
End First.
Variant of constructive choice that guarantess that the witness is greater then
some number.
Because of later use, we use a level of indirection through a finite type X
a function nat -> X and a decidable predicate on X.
Section FirstGeq.
Context{X: Type}.
Variable P : X -> Prop.
Context{decP: forall x, dec (P x)}.
Variable f: nat -> X.
Given number n <= m such that P holds at m, we con constructor
the smallest number >= n for that P holds.
Section FirstGeq.
Context {n m : nat}.
Variable (L : n <= m).
Variable (F : P (f m)).
Definition cc_nat_first_geq: nat.
Proof.
pose (P' := fun j => P (f (n + j))).
assert(exists j, P' j) as H. { exists (m - n). subst P'. cbn. now rewrite_eq (n + (m - n) = m). }
apply cc_nat_first in H.
destruct H as [k _].
exact (n + k). auto.
Defined.
Lemma cc_nat_first_geq_correct : P (f cc_nat_first_geq).
Proof.
unfold cc_nat_first_geq. cbn. now destruct cc_nat_first as [k [Q _]].
Qed.
Lemma cc_nat_first_geq_bounds : n <= cc_nat_first_geq <= m.
Proof.
unfold cc_nat_first_geq. cbn. destruct cc_nat_first as [k [_ Q]]. split; oauto.
decide (n + k <= m); auto. exfalso.
specialize (Q (m-n)). apply Q; oauto. now rewrite_eq (n + (m - n) = m).
Qed.
Lemma cc_nat_first_geq_all : forall j, n <= j < cc_nat_first_geq -> ~ P(f j).
Proof.
unfold cc_nat_first_geq. cbn. destruct cc_nat_first as [k [_ Q]].
intros j L'. specialize (Q (j - n)).
rewrite_eq (n + (j - n) = j) in Q. apply Q. omega.
Qed.
End FirstGeq.
Context {n m : nat}.
Variable (L : n <= m).
Variable (F : P (f m)).
Definition cc_nat_first_geq: nat.
Proof.
pose (P' := fun j => P (f (n + j))).
assert(exists j, P' j) as H. { exists (m - n). subst P'. cbn. now rewrite_eq (n + (m - n) = m). }
apply cc_nat_first in H.
destruct H as [k _].
exact (n + k). auto.
Defined.
Lemma cc_nat_first_geq_correct : P (f cc_nat_first_geq).
Proof.
unfold cc_nat_first_geq. cbn. now destruct cc_nat_first as [k [Q _]].
Qed.
Lemma cc_nat_first_geq_bounds : n <= cc_nat_first_geq <= m.
Proof.
unfold cc_nat_first_geq. cbn. destruct cc_nat_first as [k [_ Q]]. split; oauto.
decide (n + k <= m); auto. exfalso.
specialize (Q (m-n)). apply Q; oauto. now rewrite_eq (n + (m - n) = m).
Qed.
Lemma cc_nat_first_geq_all : forall j, n <= j < cc_nat_first_geq -> ~ P(f j).
Proof.
unfold cc_nat_first_geq. cbn. destruct cc_nat_first as [k [_ Q]].
intros j L'. specialize (Q (j - n)).
rewrite_eq (n + (j - n) = j) in Q. apply Q. omega.
Qed.
End FirstGeq.
Variant which requires m to be packed existentially
Section FirstGeqExists.
Context{n: nat}.
Variable (L: exists m, n <= m /\ P (f m)).
Definition cc_nat_first_geq_exists : nat.
Proof.
apply cc_nat in L. destruct L as [m [Q1 Q2]]. apply (cc_nat_first_geq Q1 Q2). auto.
Defined.
Lemma cc_nat_first_geq_exists_increasing : n <= cc_nat_first_geq_exists.
Proof.
unfold cc_nat_first_geq_exists. destruct cc_nat as [k [Q1 Q2]]. apply cc_nat_first_geq_bounds.
Qed.
Lemma cc_nat_first_geq_exists_correct: P (f (cc_nat_first_geq_exists)).
Proof.
unfold cc_nat_first_geq_exists. destruct cc_nat as [k [Q1 Q2]]. apply cc_nat_first_geq_correct.
Qed.
Lemma cc_nat_first_geq_exists_all : forall k, n <= k < cc_nat_first_geq_exists -> ~ P (f k).
Proof.
unfold cc_nat_first_geq_exists. destruct cc_nat as [k [Q1 Q2]]. apply cc_nat_first_geq_all.
Qed.
Lemma cc_nat_first_geq_exists_eq l : n <= l -> P ( f l) -> (forall k, n <= k < l -> ~ P (f k)) -> cc_nat_first_geq_exists = l.
Proof.
intros H1 H2 H3.
decide (cc_nat_first_geq_exists < l).
- exfalso.
apply (H3 cc_nat_first_geq_exists).
+ split; auto. apply cc_nat_first_geq_exists_increasing.
+ apply cc_nat_first_geq_exists_correct.
- decide (l < cc_nat_first_geq_exists); oauto.
exfalso. apply (cc_nat_first_geq_exists_all (k:=l)); auto.
Qed.
End FirstGeqExists.
End FirstGeq.
Context{n: nat}.
Variable (L: exists m, n <= m /\ P (f m)).
Definition cc_nat_first_geq_exists : nat.
Proof.
apply cc_nat in L. destruct L as [m [Q1 Q2]]. apply (cc_nat_first_geq Q1 Q2). auto.
Defined.
Lemma cc_nat_first_geq_exists_increasing : n <= cc_nat_first_geq_exists.
Proof.
unfold cc_nat_first_geq_exists. destruct cc_nat as [k [Q1 Q2]]. apply cc_nat_first_geq_bounds.
Qed.
Lemma cc_nat_first_geq_exists_correct: P (f (cc_nat_first_geq_exists)).
Proof.
unfold cc_nat_first_geq_exists. destruct cc_nat as [k [Q1 Q2]]. apply cc_nat_first_geq_correct.
Qed.
Lemma cc_nat_first_geq_exists_all : forall k, n <= k < cc_nat_first_geq_exists -> ~ P (f k).
Proof.
unfold cc_nat_first_geq_exists. destruct cc_nat as [k [Q1 Q2]]. apply cc_nat_first_geq_all.
Qed.
Lemma cc_nat_first_geq_exists_eq l : n <= l -> P ( f l) -> (forall k, n <= k < l -> ~ P (f k)) -> cc_nat_first_geq_exists = l.
Proof.
intros H1 H2 H3.
decide (cc_nat_first_geq_exists < l).
- exfalso.
apply (H3 cc_nat_first_geq_exists).
+ split; auto. apply cc_nat_first_geq_exists_increasing.
+ apply cc_nat_first_geq_exists_correct.
- decide (l < cc_nat_first_geq_exists); oauto.
exfalso. apply (cc_nat_first_geq_exists_all (k:=l)); auto.
Qed.
End FirstGeqExists.
End FirstGeq.
Extensionality facts for these variants of constructive choice.
Lemma cc_nat_first_geq_exists_extensional' X (P: X -> Prop) (decP: forall x, dec (P x)) (f g: nat -> X)
n (L1: exists m, n <= m /\ P (f m)) (L2: exists m, n <= m /\ P (g m)) (E: forall n, f n = g n):
~ (cc_nat_first_geq_exists L1 < cc_nat_first_geq_exists L2).
Proof.
intros L.
pose proof (cc_nat_first_geq_exists_all (L:=L2)) as H2.
specialize (H2 (cc_nat_first_geq_exists L1)).
apply H2.
- split; auto. apply cc_nat_first_geq_exists_increasing.
- rewrite <-E. apply cc_nat_first_geq_exists_correct.
Qed.
Lemma cc_nat_first_geq_exists_extensional X (P: X -> Prop) (decP: forall x, dec (P x)) (w1 w2: nat -> X)
n (L1: exists m, n <= m /\ P (w1 m)) (L2: exists m, n <= m /\ P (w2 m)) (E: forall n, w1 n = w2 n): cc_nat_first_geq_exists L1 = cc_nat_first_geq_exists L2.
Proof.
decide (cc_nat_first_geq_exists L1 < cc_nat_first_geq_exists L2) as [D|D].
- exfalso. apply (cc_nat_first_geq_exists_extensional' E D).
- decide (cc_nat_first_geq_exists L2 < cc_nat_first_geq_exists L1) as [D'|D'].
+ exfalso. apply cc_nat_first_geq_exists_extensional' in D'; auto.
+ omega.
Qed.
Section StrictMonotonicity.
Definition s_monotone (f: nat -> nat) := forall n, f n < f (S n).
Lemma s_monotone_bound f n: s_monotone f -> n <= f n.
Proof.
intros H. induction n; auto.
specialize (H n). omega.
Qed.
Lemma s_monotone_order_preserving' f n m: s_monotone f -> (n < m -> f n < f m).
Proof.
intros M L. induction L.
- apply M.
- specialize (M m). omega.
Qed.
Lemma s_monotone_order_preserving f n m: s_monotone f -> (n < m <-> f n < f m).
Proof.
intros M. split.
- now apply s_monotone_order_preserving'.
- intros L. decide (n < m)as[D'|D']; auto.
exfalso. decide (n = m) as [<-|D].
+ omega.
+ assert (m < n)as H by omega.
apply s_monotone_order_preserving' with (f:= f) in H; auto.
Qed.
End StrictMonotonicity.
Instance bounded_forall k (P:nat -> Prop) (decP: forall n, dec (P n)): dec(forall n, n <= k -> P (n)).
Proof.
induction k.
- decide (P 0) as [D|D].
+ left. intros n L. destruct n ; auto. now exfalso.
+ right. intros H. now apply D, H.
- decide (P (S k)) as [D|D].
+ destruct (IHk) as [D'|D'].
* left. intros n K. decide (n = S k); auto.
now subst n.
* right. intros H. apply D'. intros n L; auto.
+ right. intros H. now apply D, H.
Qed.
Instance bounded_exist k (P:nat -> Prop) (decP: forall n, dec (P n)): dec(exists n, n <= k /\ P (n)).
Proof.
induction k.
- decide (P 0) as [D|D].
+ left. now exists 0.
+ right. intros [n [H1 H2]]. apply D. destruct n; auto. now exfalso.
- decide (P (S k)) as [D|D].
+ left. now exists (S k).
+ destruct (IHk) as [D'|D'].
* left. destruct D' as [n [H1 H2]].
exists n. split; auto.
* right. intros [n [H1 H2]]. decide (n = S k).
-- subst n. now apply D.
-- apply D'. exists n. split; auto.
Qed.
Instance bounded_strict_forall k (P:nat -> Prop) (decP: forall n, dec (P n)): dec(forall n, n < k -> P (n)).
Proof.
destruct k.
- left. intros n L. exfalso. omega.
- apply dec_trans with (P:= forall n, n <= k -> P n); auto.
split; intros Q n L; apply Q; omega.
Qed.
Instance strict_bounded_exist k (P:nat -> Prop) (decP: forall n, dec (P n)): dec(exists n, n < k /\ P (n)).
Proof.
destruct k.
- right. intros [n [L _]]. omega.
- apply dec_trans with (P:= exists n, n <= k /\ P n); auto.
split; intros [n [L Q]]; exists n; split; oauto.
Qed.
Languages
Treat predicates as "languages". This simplifies some things as one does not always write out the forall quantifier for equivalence etc. We register languages for setoid rewriting.Section Languages.
Variable (X:Type).
Definition Language := X -> Prop.
Definition empty_language : Language := fun _=> False.
Definition universal_language : Language := fun _ => True.
Definition language_inclusion (P Q :Language) :=
forall w, P w -> Q w.
Definition language_eq (P Q: Language) := (forall w, P w <-> Q w).
Definition language_union (P Q: Language) : Language:= fun w => P w \/ Q w.
Definition language_intersection(P Q: Language): Language:= fun w => P w /\ Q w.
Definition language_complement (P : Language) :Language := fun w => ~ (P w).
Definition language_difference (P Q : Language) : Language := fun w => P w /\ ~ Q w.
End Languages.
Arguments empty_language {X} _.
Arguments universal_language {X} _.
Notation "x <$= y" := (language_inclusion x y) (at level 70).
Notation "x =$= y" := (language_eq x y) (at level 70).
Notation "x \$/ y" := (language_union x y) (at level 69).
Notation "x /$\ y" := (language_intersection x y) (at level 69).
Notation "x ^$~ " := (language_complement x) (at level 68).
Notation "{}" := (empty_language) (at level 20).
Hint Unfold language_intersection.
Hint Unfold language_union.
Hint Unfold language_complement.
Hint Unfold language_eq.
Hint Unfold language_inclusion.
Hint Unfold empty_language.
Hint Unfold universal_language.
Section LanguageLemmata.
Variable X:Type.
Variables L L_1 L_2 : Language X.
Lemma language_empty_iff : L =$= {} <-> (forall w, ~ (L w) ).
Proof. firstorder. Qed.
Lemma language_universal_iff : L =$= universal_language <-> (forall w, L w).
Proof. firstorder. Qed.
Lemma language_eq_iff : L_1 =$= L_2 <-> L_1 <$= L_2 /\ L_2 <$= L_1.
Proof. firstorder. Qed.
Lemma language_eq_symmetric: L_1 =$= L_2 <-> L_2 =$= L_1.
Proof. firstorder. Qed.
Lemma language_union_comm: L_1 \$/ L_2 =$= L_2 \$/ L_1.
Proof. firstorder. Qed.
Lemma language_intersection_comm: L_1 /$\ L_2 =$= L_2 /$\ L_1.
Proof. firstorder. Qed.
End LanguageLemmata.
Instance language_eq_equivalence X: Equivalence (@language_eq X).
Proof. constructor; firstorder. Qed.
Instance language_eq_mem X w: Proper (@language_eq X ==> iff) (fun L => L w).
Proof. firstorder. Qed.
Instance language_incl X: Proper (@language_eq X ==> @language_eq X ==> iff) (@language_inclusion X).
Proof. firstorder. Qed.
Instance language_union_proper X: Proper (@language_eq X ==> @language_eq X ==> @language_eq X) (@language_union X).
Proof. firstorder. Qed.
Instance language_intersection_proper X: Proper (@language_eq X ==> @language_eq X ==> @language_eq X) (@language_intersection X).
Proof. firstorder. Qed.
Instance language_difference_proper X: Proper (@language_eq X ==> @language_eq X ==> @language_eq X) (@language_difference X).
Proof. firstorder. Qed.
Instance language_complement_proper X: Proper (@language_eq X ==> @language_eq X) (@language_complement X).
Proof. firstorder. Qed.
Instance dec_pair (X Y : Type) (P : X -> Y -> Prop) (decP: forall x y , dec (P x y)): forall z, dec (match z with (x,y) => P x y end ).
Proof.
intros [x y]. auto.
Qed.
Instance dec_sum (X Y : Type) (P: X -> Prop) (Q: Y -> Prop) (decP: forall x, dec (P x)) (decQ: forall y, dec (Q y)):
forall z,dec ( match z with
|inl x => P x
|inr y => Q y end).
Proof.
intros [x|y]; auto.
Qed.
Instance dec_option (X : Type) (P1 : X -> Prop) (P2: Prop) (decP1: forall x , dec (P1 x))(decP2: dec P2):
forall z, dec (match z with
| None => P2
| Some x => P1 x end).
Proof.
intros [x|]; auto.
Qed.
Instance dec_destruct_list (X: Type) (P1 : Prop) (P2: X -> list X -> Prop)
{decP1: dec P1}{decP2: forall x l , dec (P2 x l)} (l:list X):
dec (match l with
| [] => P1
| a::l => P2 a l
end ).
Proof.
destruct l ;auto.
Qed.
Instance dec_match_bool (P1 P2 : Prop) {decP1: dec P1}{decP2: dec P2 } (b: bool):
dec (match b with
| false => P1
| true => P2
end ).
Proof.
destruct b ;auto.
Qed.
Lemmas for Numbers
Lemma complete_induction (P : nat -> Prop) : P 0 -> (forall n, (forall m, m <= n -> P m) -> (P (S n))) -> forall n, P n.
Proof.
intros p0 pS.
enough (forall n, forall m, m <= n -> P m).
- intros n. apply (H n n). omega.
- induction n; intros m L.
+ now rewrite_eq (m = 0).
+ decide (m = S n) as [D|D].
* rewrite D. apply pS. apply IHn.
* apply IHn. omega.
Qed.
Lemma max_le_left n m k: k <= n -> k <= max n m.
Proof.
intros L.
pose (p := (Nat.le_max_l n m)).
omega.
Qed.
Lemma max_le_right n m k : k <= m -> k <= max n m.
Proof.
intros L. rewrite Nat.max_comm. now apply max_le_left.
Qed.
Lemma max_le k m n : k <= max m n -> k <= m \/ k <= n.
Proof.
destruct (Nat.max_dec m n) as [D|D]; rewrite D; tauto.
Qed.
Lemma mul_ge_0 n m : n> 0 -> m > 0 -> n * m > 0.
Proof.
intros L1 L2. apply Nat.lt_0_mul'; split; omega.
Qed.
Lemma pow_ge_zero i : Nat.pow 2 i > 0.
Proof.
induction i; cbn; omega.
Qed.
Equality of Vectors
Lemma list_eq (X: Type) (l1 l2: list X) : (forall n, nth_error l1 n= nth_error l2 n) -> l1 = l2.
Proof.
revert l2. induction l1; intros l2 EE.
- specialize (EE 0). cbn in EE. now destruct l2.
- destruct l2.
+ now specialize (EE 0).
+ f_equal.
* specialize (EE 0). cbn in EE. congruence.
* apply IHl1.
intros n. specialize (EE (S n)). now cbn in EE.
Qed.
Notation "A ^^ l" := (A^(finType_fromList l)) (at level 30).
Lemma vector_eq (X Y: finType) (a b : X^Y) : (forall y, applyVect a y = applyVect b y) -> a = b.
Proof.
intros E.
apply vector_extensionality.
rewrite <-(vectorise_apply_inverse a).
rewrite <-(vectorise_apply_inverse b). cbn.
unfold getImage. apply list_eq.
induction (elem Y); intros n; cbn; auto.
destruct n; cbn; auto using IHl. now f_equal.
Qed.