## Stream: Coq users

### Topic: How to simplify ?

#### pianke (May 17 2023 at 08:07):

H : f a b = true ->
a = b
goal: f a b = true

#### Laurent Théry (May 17 2023 at 09:24):

What you want to simplify?

#### Paolo Giarrusso (May 17 2023 at 09:26):

unclear question but for an unknown `f`, that hypothesis will not help at all to prove the goal

#### pianke (May 17 2023 at 11:08):

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

#### Enrico Tassi (May 17 2023 at 11:09):

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

#### Paolo Giarrusso (May 17 2023 at 11:17):

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.

#### pianke (May 17 2023 at 11:43):

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

#### Pierre Castéran (May 17 2023 at 15:05):

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

#### Paolo Giarrusso (May 17 2023 at 16:42):

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

#### Paolo Giarrusso (May 17 2023 at 16:44):

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.

#### Huỳnh Trần Khanh (Jun 05 2023 at 00:41):

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

#### Huỳnh Trần Khanh (Jun 05 2023 at 00:43):

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