Ssreflect Users Discussion List

[Frederic Chyzak <>]

Hi,

On Sun, 2014-11-30 at 11:34 -0500, Arthur Azevedo de Amorim wrote:
> Suppose that I have a goal such as
> 
> Goal [forall b : bool, b == (0 < (b : nat))].
> 
> What is the best way of solving this goal with computation? I.e. I
> want to expand/rewrite all the definitions so that this goal becomes
> solvable by reflexivity.

I don't know what the "best" way means to you, but I will try one
answer.

To close your goal, you don't need to do any definition expansion
manually on this example: [by case] will solve the goal by itself, and
it is the expected idiom here.  Indeed, [case] splits the goal into the
two subcases [b = true] and [b = false], then [by ...] is there to
unfold sufficiently many definitions and solve each subgoal by easy
means (including computation and reflexivity).

But if you really insist in solving this goal by decomposing what is
going on, I guess you will have a pretty detailed view of the kind of
steps automated by [by ...] if you step through the attached script.

In it, I suggest [Set Printing Coercions] to see some hidden computing
functions that cannot be imagined otherwise.  Besides, most of the
definitions that I have unfolded are those of constants whose names are
hidden by notations: I would not have known them without doing [Set
Printing All] occasionally.

Hope this helps,
Frédéric

Require Import ssreflect ssrbool eqtype ssrnat.

Set Printing Coercions.
(*Set Printing All.*)

Lemma foo : forall b : bool, b == (0 < (b : nat)).
Proof.
(* by case. *)
move=> b.
case: b.
  rewrite [nat_of_bool _]/=.
  rewrite /leq.
  rewrite /subn.
  rewrite /=.
  rewrite [_ nat_eqType]/eq_op.
  rewrite /=.
  rewrite [_ bool_eqType]/eq_op.
  rewrite /=.
  rewrite /eqb.
  rewrite /negb.
  rewrite /addb.
  rewrite /is_true.
  reflexivity.
rewrite [nat_of_bool _]/=.
rewrite /leq.
rewrite /subn.
rewrite /=.
rewrite [_ nat_eqType]/eq_op.
rewrite /=.
rewrite [_ bool_eqType]/eq_op.
rewrite /=.
rewrite /eqb.
rewrite /negb.
rewrite /addb.
rewrite /is_true.
reflexivity.
Qed.