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?

pianke (Jun 03 2023 at 18:03):

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: Oct 04 2023 at 20:01 UTC