When I prove a theorem in Coq, I made a hypothesis that is 'False', and by using 'contradiction' tactics, I finish my proof.
However, the coq program show some words for me.
All the remaining goals are on the shelf:
positive
What is this, and how can I deal with it?
Edit : I wrote my code here. The last lemma has a problem.
Edit2 : With Jason Rute's advice, my proble is solved.
From mathcomp Require Import all_ssreflect.
Require Import QArith.
Axiom excluded_middle :
forall P : Prop, P \/ not P.
Lemma all_prop (S : Set) (P : S -> Prop) :
(forall x : S, (P x)) <-> not (exists x : S, not (P x)).
Proof.
split.
{ unfold not. intros. destruct H0 as [x Hx].
apply Hx. apply H. }
{ unfold not. intros.
specialize (excluded_middle (P x)) as Hx.
destruct Hx. { exact H0. }
{ destruct H. exists x. exact H0. } }
Qed.
Lemma not_not_equiv (P : Prop) :
P <-> (not (not P)).
Proof.
split.
{ unfold not. intros. apply H0 in H. exact H. }
{ unfold not. intros.
specialize (excluded_middle P) as HP. destruct HP.
{ exact H0. } { apply H in H0. contradiction. } }
Qed.
Lemma not_all_prop (S : Set) (P : S -> Prop) :
not (forall x : S, (P x)) <-> exists x : S, not (P x).
Proof.
rewrite all_prop. symmetry. apply not_not_equiv.
Qed.
Lemma not_exists_prop (S : Set) (P : S -> Prop) :
not (exists x : S, (P x)) <-> forall x : S, not (P x).
Proof.
symmetry. rewrite all_prop.
setoid_rewrite <- not_not_equiv. reflexivity.
Qed.
(* 1 # n is equal to 1/n *)
Lemma Archimedean :
forall q : Q, 0 < q ->
exists n : positive, 1 # n < q.
Proof.
intros. destruct q. exists (Qden + 1)%positive. unfold Qlt. simpl.
specialize (Zgt_succ (Z.pos Qden)) as H0. simpl in H0.
apply Z.gt_lt in H0. setoid_rewrite <- Zmult_1_l at 1.
apply Zmult_lt_compat2.
{ assert (H1 : (0 < Qnum)%Z).
{ unfold Qlt in H. simpl in H. rewrite Zmult_1_r in H. exact H. }
specialize (Zlt_le_succ _ _ H1) as H2. simpl in H2.
split. by []. exact H2. }
{ split. by []. exact H0. }
Qed.
Lemma Pos_max_four (a b c d : positive) :
exists x : positive, (a <= x /\ b <= x /\ c <= x /\ d <= x)%positive.
Proof.
exists (Pos.max (Pos.max a b) (Pos.max c d)). repeat split.
{ apply Pos.le_trans with (Pos.max a b)%positive.
apply Pos.le_max_l. apply Pos.le_max_l. }
{ apply Pos.le_trans with (Pos.max a b)%positive.
apply Pos.le_max_r. apply Pos.le_max_l. }
{ apply Pos.le_trans with (Pos.max c d)%positive.
apply Pos.le_max_l. apply Pos.le_max_r. }
{ apply Pos.le_trans with (Pos.max c d)%positive.
apply Pos.le_max_r. apply Pos.le_max_r. }
Qed.
Lemma Pos_max_le_l (a b c : positive) :
(Pos.max a b <= c -> a <= c)%positive.
Proof.
intros.
apply Pos.le_trans with (Pos.max a b)%positive.
apply Pos.le_max_l. exact H.
Qed.
Lemma Pos_max_le_r (a b c : positive) :
(Pos.max a b <= c -> b <= c)%positive.
Proof.
intros.
apply Pos.le_trans with (Pos.max a b)%positive.
apply Pos.le_max_r. exact H.
Qed.
Definition compare (f g : positive -> Q) :=
exists s : positive, (forall n m : positive,
(s <= n)%positive -> (s <= m)%positive -> f n <= g m).
Definition get_closer (f g : positive -> Q) :=
forall n : positive, (exists m : positive,
(forall p : positive, (m <= p)%positive -> g p - f p < 1 # n) ).
Record P := mkP {
l : positive -> Q;
r : positive -> Q;
Cond1 : compare l r;
Cond2 : get_closer l r;
}.
Definition Plt (X Y : P) :=
forall s : positive, (exists n m : positive,
(s <= n)%positive /\ (s <= m)%positive /\
(r X) n < (l Y) m).
Lemma Plt_equiv (X Y : P) :
compare (l Y) (r X) <-> not (Plt X Y).
Proof.
unfold compare, Plt. split.
{ unfold not. intros. destruct H as [s Hs].
destruct (H0 s) as [n [m [H1 [H2 H3]]]].
specialize (Hs m n H2 H1) as H4.
specialize (Qlt_le_trans _ _ _ H3 H4) as H5.
apply Qlt_irrefl in H5. exact H5. }
{ rewrite not_all_prop. intros [x Hx]. rewrite not_exists_prop in Hx.
exists x. intros. specialize (Hx m) as H1.
rewrite not_exists_prop in H1. specialize (H1 n) as H2.
destruct (Qlt_le_dec (r X m) (l Y n)) as [Hdec|Hdec]; first last.
{ exact Hdec. } { unfold not in H2.
assert (H3 : (x <= m)%positive /\ (x <= n)%positive /\ r X m < l Y n).
{ repeat split. exact H0. exact H. exact Hdec. }
apply H2 in H3. contradiction. } }
Qed.
Lemma Peq_trans_half (a b c : P) :
not (Plt a b) -> not (Plt b c) -> not (Plt a c).
Proof.
rewrite -Plt_equiv. rewrite -Plt_equiv.
unfold compare, not, Plt. intros.
destruct H as [s Hs], H0 as [t Ht].
destruct (H1 (Pos.max s t)) as [n [m [H2 [H3 H4]]]].
rewrite Qlt_minus_iff in H4.
destruct (Archimedean _ H4) as [u Hu].
destruct ((Cond2 b) u) as [v Hv].
specialize (Pos_max_four s t v) as [x [H5 [H6 [H7 _]]]].
specialize (Hv _ H7) as H8.
specialize (Hs x n H5 (Pos_max_le_l _ _ _ H2)) as H9.
specialize (Ht m x (Pos_max_le_r _ _ _ H3) H6) as H10.
apply Qopp_le_compat in H9.
specialize (Qlt_trans _ _ _ H8 Hu) as H11.
specialize (Qplus_le_compat _ _ _ _ H10 H9) as H12.
specialize (Qlt_le_trans _ _ _ H11 H12) as H13.
apply Qlt_irrefl in H13. exact H13. Unshelve.
Admitted.
Unshelve
tactic: coq.inria.fr/refman/proofs/writing-proofs/… $\endgroup$positive
, likexH
. Soexact xH.
if I understand the situation. $\endgroup$