search

math-comp / mcb

Mathematical Components (the Book)
Other
140 stars 25 forks source link

§4.1.3: Lemma example uses andP view, which won't work with current definition of reflect #20

Closed anton-trunov closed 5 years ago

anton-trunov commented 7 years ago

Up until §4.1.3 every lemma can be proved using the temporary definition of reflect from §4.1.1. I think to avoid confusion, the book should mention that we need "real" reflect to use move=> lekn/andP..

gares commented 5 years ago

I'm triaging the issues here, and I'm not 100% sure I this one. In particular this code works:

Require Import ssreflect Bool.

Inductive re (P : Prop) (b : bool) : Prop :=
  | ReT (p : P) (e : b = true)
  | ReF (np : ~ P) (e : b = false).

Axiom andP : forall (b1 b2 : bool), re (b1 = true /\ b2 = true) (b1 &&b2).
Axiom elimTF : forall (P : Prop) (b c : bool), re P b -> b = c -> if c then P else ~ P.

Hint View elimTF|3.

Goal (true && false) = true -> False.
move=> /andP.

The only difference with the book is that elimTF has not a extra parameter Q (I'm removing it in the commit fixing this issue). I guess you tried and got an error message.