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?

I'm not sure if this makes sense..

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)

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

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

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

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`

...

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`

.

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?

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

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