H : f a b = true ->

a = b

goal: f a b = true

What you want to simplify?

unclear question but for an unknown `f`

, that hypothesis will not help at all to prove the goal

I want to apply H. Because goal statement is same as H.

Isn't the type of H `f a b = true -> a = b`

?

you could apply `H : a = b -> f a b = true`

, but apparently you have the _converse_ implication `H : f a b = true -> a = b`

, so "applying H" doesn't make any sense.

Where f checks the bool equality of two numbers. Or may i write it as H : f ab && f cd = true .

a=b &&c=d

The best would be to post the script which led to this (partially presented) sub-goal.

Otherwise, the answer could only be "depends on the context".

pianke said:

Where f checks the bool equality of two numbers. Or may i write it as H : f ab && f cd = true .

a=b &&c=d

that is much better, especially because instead of `->`

you have `&&`

— you can turn ` f ab && f cd = true `

into ` f ab = true /\ f cd = true `

with lemma `andb_true_iff,`

, and if `f`

is (say) the stdlib's `Nat.eqb`

, you can turn `f a b = true`

into `a = b`

with `Nat.eqb_eq.`

:

```
From Coq Require Import Bool Arith.
Lemma foo a b c d : Nat.eqb a b && Nat.eqb c d = true -> a = b /\ c = d.
Proof.
(* How I found those lemmas:
Search (_ && _ = true).
Search Nat.eqb.
*)
now rewrite ->andb_true_iff, !Nat.eqb_eq.
Qed.
```

but I agree with the others: you typically make helping you harder than needed and it's not clear why. Did a teacher forbid you from sharing partial solutions?

No,not at all.

then start posting more details from now on, this will end up saving time for you

the easiest way is to Ctrl+A and Ctrl+C in the text editor then in here type 3 backticks followed by a newline, hit Ctrl+V, then type another 3 backticks on a new line and send

Last updated: Jun 25 2024 at 15:02 UTC