Ssreflect Users Discussion List

[Georges Gonthier <>]

  This is really a infelicitous conjunction of usually convenient overloading 
that happen to conflict.
The view (@id (_ /\ _)), which is intended as a way of checking that the top 
assumption indeed is an 'and', before destructing.
Unfortunately it has type (?U /\ ?V -> ?U /\ ?V), whose conclusion happens to 
unify with (_ <-> _),
one of the equivalences supported by view lemmas in ssreflect.v (the Coq 
standard prologue uses Definition rather than Inductive to declare iff).
The ssreflect view implementation thus finds it can use the iffLR view, 
interpreting (@id (_ /\ _)) as (@id ((A /\ B) <-> ?P)), and replacing the top 
assumption H with (fun P (E : A /\ B <-> P) => iffLR (id E) H) : (forall P, 
(A /\ B <-> P) -> P) which is indeed not a quantified inductive.
   The simplest way to achieve you ends reliably is to protect the and 
inductive under a different one, e.g.,
case/(@Wrap (_ /\ _))=> -[] ...
    -- Georges

-----Original Message-----
From:  
[] On Behalf Of Enrico Tassi
Sent: 26 June 2014 16:50
To: 
Subject: Re: [ssreflect] Why does [case/(@id (and _ _))] tell me that [and] 
is not an inductive product?

On Thu, Jun 26, 2014 at 04:34:27PM +0100, Jason Gross wrote:
> Hi,
> The following code fails with "Error: Not an inductive product":
> 
> Require Import ssreflect. (* v 1.4 *)
> Goal forall A B, A /\ B -> True.
>     move => A B.
>     case/(@id (and _ _)).

I hope that this decompilation helps you understand what goes wrong:

  Goal forall A B, A /\ B -> True.
  move => A B.
  have xx := @id (and _ _).
  move/xx.
  case.

Given that "xx : forall P P0 : Prop, P /\ P0 -> P /\ P0", the first premise 
"A /\ B" can play the role of P, being of type Prop.

But the real question is: what are you trying to do?

Best,
--
Enrico Tassi