## Stream: Coq users

### Topic: Simple contradiction proof in ssreflect

#### 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?

#### Julin Shaji (Nov 21 2023 at 06:58):

I'm not sure if this makes sense..

#### 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)

#### 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).

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

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

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

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

#### 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?

#### Julin Shaji (Nov 21 2023 at 16:14):

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

#### 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