Stream: Coq users

Topic: ✔ Is True a neutral element for and?

Julien Puydt (Dec 12 2022 at 13:55):

The question appeared in a MC setting, but it's really about Coq.

During one of my experimental proofs, a rewrite (propT H314159). made a True /\ ... appear within the goal.

I found how to rewrite/simplify the equivalent for booleans (andb_true_l), but nothing for Prop. I searched both using (True /\ _) and using left_id , but nothing turned up.

I ended up using a have foo: ... then rewrite foo; clear foo, which is pretty ugly.

Did I miss something obvious or is there something missing?

Karl Palmskog (Dec 12 2022 at 13:56):

one option is to use AAC Tactics with the Prop instances: https://github.com/coq-community/aac-tactics/blob/master/theories/Instances.v#L206

Paolo Giarrusso (Dec 12 2022 at 14:18):

By default True /\ P = P fails and you only get True /\ P <-> P — might be too restrictive for ssrfun.left_id? Definition left_id e op := forall x, op e x = x.

Karl Palmskog (Dec 12 2022 at 14:22):

right, the AAC stuff only works under the iff relation. I don't think many people do much reasoning under = on Prop?

Paolo Giarrusso (Dec 12 2022 at 14:24):

mostly I was pointing out why an ssreflect left_id lemma can't be proven (in axiom-free Coq).

Paolo Giarrusso (Dec 12 2022 at 14:26):

@Julien Puydt BTW, rewrite foo; clear foo is rewrite {}foo, and there's even rewrite (_ : A = B) (or here rewrite (_ : A <-> B))

Julien Puydt (Dec 12 2022 at 19:07):

Ok, so now it's:

have foo: forall P: Prop, (True /\ P) <-> P.
  move=> P.
  split.
    by move=> [_ -].
  by [].
rewrite {}foo.

but indeed I didn't use an equality but equivalence, so left_idwasn't a good search.

So, should I report it as wishlist issue against Coq?

Notification Bot (Dec 14 2022 at 12:13):

Julien Puydt has marked this topic as resolved.

Last updated: Oct 04 2023 at 23:01 UTC