```
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?

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 `H0`

are 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.

```
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.
```

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`

.

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).

`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.
```

```
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.
```

I can write in this way?

```
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?
```

I want to prove a1<a2 < a3 from above.

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.
```

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)?

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)

Lemma a123: forall a1 a2 a3,

(a1 < a2) -> ( a2 < a3 )->(a1 < a3).

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.

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.
```

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.

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.

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 )).

The easiest way to solve such goals is to use the `lia`

tactic (after `Require Import Lia`

).

Ok,It solved the problem.Thank you.

Last updated: Jun 24 2024 at 13:02 UTC