Stream: Coq users

Topic: Simple contradiction proof in ssreflect


view this post on Zulip Julin Shaji (Nov 21 2023 at 06:55):

I was trying to prove this with ssreflect:

  Goal
  (Some false = Some true) = is_true true -> 1==2.
  Proof.
    move=>H.

How can I say that (Some false = Some true) = true as assumption can be used to prove anything?

view this post on Zulip Julin Shaji (Nov 21 2023 at 06:58):

I'm not sure if this makes sense..

view this post on Zulip Kenji Maillard (Nov 21 2023 at 09:46):

The type is_true true reduces to true = true that you can inhabit with eq_refl, so using transport/rewriting along the equality H you can obtain an inhabitant of Some false = Some true. Now it is not hard to prove that Some false = Some true -> False and use destruct on the result:

Lemma no_confusion_Some_bool : Some false = Some true -> False.
Proof. discriminate. Qed.

Goal (Some false = Some true) = is_true true -> 1 = 2.
Proof.
  intros H.
  assert (h : Some false = Some true) by (rewrite H; reflexivity).
  destruct (no_confusion_Some_bool h).

  (* Or simply *)
  (* intros H; enough (Some false = Some true) by discriminate; now rewrite H. *)
Qed.

(reformulated without dependence on mathcomp because I didn't have it at hand)

view this post on Zulip Meven Lennon-Bertrand (Nov 21 2023 at 09:48):

Note, though, that in general, equalities between propositions (here, the propositions are Some false = Some true and is_true true) are not a good notion. To assert that Some false is equal to Some true, you should simply use Some false = Some true. In a sense, it is like doing if (b = true) then … instead of if b then … in your favorite programming language. Except this is worse, because Coq's Prop behaves rather differently than booleans, and in general manipulating equalities between propositions is a rather weird thing to do (and in particular, tactics are not geared towards easy manipulations of these).

view this post on Zulip Pierre Jouvelot (Nov 21 2023 at 12:29):

FYI, the solution provided @Kenji Maillard can be rewritten in ssreflect as, for instance:

Goal (Some false = Some true) = is_true true -> 1 = 2.
Proof.
have no_confusion_Some_bool : Some false = Some true -> false by case.
by move=> H; have/no_confusion_Some_bool : Some false = Some true by rewrite H.
Qed.

view this post on Zulip Cyril Cohen (Nov 21 2023 at 12:53):

@Julin Shaji I must first say that @Meven Lennon-Bertrand is right and that it is very surprising to me that one even lands in this kind of goal by using ssreflect, there is probably a simplification to perform in the begining of the proof script you might be in, in order to get something more... ssreflectish.

Now here is a shortest ssreflect script I could think of:

Goal (Some false = Some true) = is_true true -> 1 == 2.
Proof. by move=> e; suff: true by rewrite -e. Qed.

indeed ssreflect's by does the discrimination already, so it suffices to use true as a support for performing the rewriting of the equation.

view this post on Zulip Julin Shaji (Nov 21 2023 at 16:03):

Cyril Cohen said:

Julin Shaji I must first say that Meven Lennon-Bertrand is right and that it is very surprising to me that one even lands in this kind of goal by using ssreflect, there is probably a simplification to perform in the begining of the proof script you might be in, in order to get something more... ssreflectish

Heh, heh.. Actually, I think the problem was that I mixed up induction tactic in between the ssreflect stuff. Could that be a possible cause?

I was sort annoyed by elim refusing to proceed if variable is already in the assumptions part. induction didn't have a problem with that.

And induction automatically adds induction hypothesis to the assumption section.

I guess this is a good time to know why ssreflect style uses elim instead of induction...

view this post on Zulip Cyril Cohen (Nov 21 2023 at 16:08):

The main reason is that induction names hypotheses for you, which is not stable. You can discharge variables from the context in the same line using elim: x H1 H2 ... Hn.

view this post on Zulip Julin Shaji (Nov 21 2023 at 16:13):

Cyril Cohen said:

You can discharge variables from the context in the same line using elim: x H1 H2 ... Hn.

In some situations, where the value being inducted upon is used in one of the assumptions, elim won't allow me to do induction. Is there a way around that?

Should we be bringing those assumptions back to the goal part?

view this post on Zulip Julin Shaji (Nov 21 2023 at 16:14):

Error goes like: 'var is used in hypothesis H.'

view this post on Zulip Cyril Cohen (Nov 21 2023 at 16:37):

Julin Shaji said:

Cyril Cohen said:

You can discharge variables from the context in the same line using elim: x H1 H2 ... Hn.

In some situations, where the value being inducted upon is used in one of the assumptions, elim won't allow me to do induction. Is there a way around that?

Should we be bringing those assumptions back to the goal part?

That is what the H1 ... Hn part is doing


Last updated: Jun 23 2024 at 05:02 UTC