relation between 3 variables · Coq users

H : (a3 <? a1) = false
H0 : (a1 <? a2) = true
H1 : (a2 <? a3) = true

From H0 & H1 (a1 <? a3)=true.

Now H & H1 are contra statements? We can find any contra statement among above hypothesis, on the basis of which I close any sub lemma?

Andrés Goens (Aug 29 2021 at 06:44):

I don't really understand your question, what do you want to prove (or disprove)? What do you mean with contra statements? In your example H and H0are not in contradiction. What subgoal you can close depends on what your statement is.

Try it with pen and paper, the three hypotheses you have there are pretty straightforward. Then we can see if the question is about order relations/propositional logic or about how to get Coq to understand your pen and paper conclusion.

zohaze (Aug 29 2021 at 07:34):

Q1) H4 : (a1 <? a3) = true
      H6 : (a3 <? a1) = true .
It should solve by lia. But if not then what command I should apply?

Q2)  H : (a3 <? a1) = false->
        (a3 <? a2) = false & (a2<? a1)=false ?
  It is necessary that H is false then other two relation also false. Is it possible
that relation( (a3 <? a2)   or (a2<? a1))  may be true.

Olivier Laurent (Aug 29 2021 at 10:21):

It is probably a good idea to first move to _ < _ statements rather than (_ <? _) = _ statements.
Q1)

Goal forall a b, (a <? b) = true -> (b <? a) = true -> False.
Proof.
intros a b.
rewrite ? Nat.ltb_lt.
apply Nat.lt_asymm.
Qed.

Q2) Do you mean, is it possible to have a1 <= a3 together with a3 < a2 or a2 < a1? if so the answer is yes: a1 = 0, a2 = 1, a3 = 0.

zohaze (Aug 29 2021 at 12:21):

Thank you. H1 : (a3 <? a1) = false
H2 : (a1 <? a2) = true
H2 : (a2 <? a3) = true
From above I can write a1 <? a3=true.
Any more information I can extract from above(especially related to H1).

Olivier Laurent (Aug 29 2021 at 14:58):

H1 gives you a1 <= a3 (by rewrite Nat.ltb_ge).
But, by transitivity, H2 and H3 give you the strictly stronger a1 < a3.

Goal forall a1 a2 a3,
  (a3 <? a1) = false -> (a1 <? a2) = true -> (a2 <? a3) = true -> a1 < a3.
Proof.
intros a1 a2 a3.
rewrite ? Nat.ltb_lt, Nat.ltb_ge.
intros H1 H2 H3.
apply (Nat.lt_trans _ _ _ H2 H3).
Qed.

Olivier Laurent (Aug 29 2021 at 15:00):

Goal forall a1 a2 a3,
   (a1 <? a2) = true -> (a2 <? a3) = true -> (a3 <? a1) = false.
Proof.
intros a1 a2 a3.
rewrite ? Nat.ltb_lt, Nat.ltb_ge.
intros H2 H3.
apply Nat.lt_le_incl.
apply (Nat.lt_trans _ _ _ H2 H3).
Qed.

zohaze (Aug 31 2021 at 01:31):

Lemma check_rel : forall a1 a2 a3,
(a3 <? a1 = false)->
(a2 <? a3) = true->
(a2 <? a1 = false).
a3=5 a1=3 a2=4

Lemma check_rel2: forall a1 a2 a3,
( a3 <? a1 = true).
To prove above relation,I need
 (a3 <? a2) = true &(a2 <? a1 = true).
 Any other combination can give this result?

Olivier Laurent (Aug 31 2021 at 09:31):

If you want to contradict that forall a1 a2 a3, (a3 <? a1 = false) -> (a2 <? a3) = true -> (a2 <? a1 = false). You can proceed as follows:

Goal ~(forall a1 a2 a3, (a3 <? a1 = false) -> (a2 <? a3) = true -> (a2 <? a1 = false)).
Proof.
intros H.
specialize H with 3 2 5.
cbn in H.
assert (true = false) as Hn by tauto.
inversion Hn.
Qed.

Concerning your second point, I am not sure to understand what is your goal. If you want to prove forall a1 a2 a3, (a3 <? a2 = true) -> (a2 <? a1 = true) -> (a3 <? a1 = true), you can do:

Lemma check_rel2: forall a1 a2 a3, (a3 <? a2 = true) -> (a2 <? a1 = true) -> (a3 <? a1 = true).
Proof.
intros a1 a2 a3.
rewrite ? Nat.ltb_lt, ? Nat.ltb_ge.
apply Nat.lt_trans.
Qed.

zohaze (Aug 31 2021 at 15:15):

If I write lemma that (a1 <?a2)=true-> (a2<?a3)=true->(a1<?a3)=true then true else false. Now compare above conditions with lemma. 1 or 2 Conditions are against lemma/contradictory to lemma((a3 <? a1 = false) -> (a2 <? a3) = true -> (a2 <? a1 = false)). How I can close goal now(It would be more general)?

Olivier Laurent (Aug 31 2021 at 15:48):

I do not follow you. Could you write a complete Coq statement: Lemma xxx : xxx.?
(possibly relying on < and <= rather than <? would be easier to follow)

zohaze (Aug 31 2021 at 16:25):

H1 : (a3 < a1)
H2 : (a1 < a2)
H3 : (a2 < a3). Only valid relation between 3 are in lemma(a123) . Any other relation among 3 is not valid.
Now in H1 (a3 <a1) is wrong . How to link H1 is against lemma,therefore it gives false.

I want to write in this way(is it possible?) Lemma r1_r3: forall r1 r2 r3,
((r1 <? r2) = true->
( r2 <? r3 = true)->
(r1 <? r3) = true)=true <->( _ <? _=false)=false.

Olivier Laurent (Aug 31 2021 at 17:40):

I am still not sure this is what you are looking for, but in the spirit of what is above you can do:

Lemma a123' : forall a1 a2 a3, a1 < a2 -> a2 < a3 -> ~(a3 < a1).
Proof.
intros a1 a2 a3 H2 H3 H1.
apply (Nat.lt_asymm _ _ H1).
apply (Nat.lt_trans _ _ _ H2 H3).
Qed.

Goal forall a1 a2 a3, (a1 <? a2 = true) -> (a2 <? a3 = true) -> (a3 <? a1 = false).
Proof.
intros a1 a2 a3.
rewrite ? Nat.ltb_lt, ? Nat.ltb_ge.
intros H2 H3.
apply Nat.nlt_ge.
apply (a123' _ _ _ H2 H3).
Qed.

zohaze (Sep 01 2021 at 17:45):

Yes. Now I can say something about a relation (true or false). I have asserted above lemma.Situation is like this
H1 : (a3 <? a1) = false
H2 : (a1 <? a2) = true
H3 : (a2 <? a3) = true
H4 : (a1 <? a2) = true -> (a2 <? a3) = true -> (a3 <? a1) = false
How I can find contradiction here or without applying assert command how I can relate above lemma with H1 H2 H3 so that on the basis of contradiction close sub lemma.

Olivier Laurent (Sep 01 2021 at 18:25):

I do no see what you want: H4 is useless here since it allows to derive H1 from H2 and H3, but since you already have H1, you can clear H4. And you cannot derive a contradiction from H1, H2, H3 and H4 since a1 = 0, a2 = 1, a3 = 2 satisfies them all.

zohaze (Sep 03 2021 at 01:24):

If Lemma (123' : forall a1 a2 a3, a1 < a2 -> a2 < a3 -> ~(a3 < a1) )holds then result of addition among elements is also true.We can prove it? ( Lemma a123'' : forall a1 a2 a3 , a3 - a1 <= a2 - a1 + (a3 - a2 )).

Olivier Laurent (Sep 03 2021 at 08:11):

The easiest way to solve such goals is to use the lia tactic (after Require Import Lia).

Stream: Coq users

Topic: relation between 3 variables

zohaze (Aug 29 2021 at 06:11):