The Coq mailing list

[Hussain Sobhy <hussain.sob7y AT gmail.com>]

Further down in the tutorial, there's this example:

Inductive ex (A:Type) (P:A -> Prop) : Prop :=
  ex_intro : forall x:A, P x -> ex (A:=A) P.

Notation "'exists' x .. y , p" := (ex (fun x => .. (ex (fun y => p)) ..))
  (at level 200, x binder, right associativity,
   format "'[' 'exists'  '/  ' x  ..  y ,  '/  ' p ']'")
  : type_scope.

Definition basic_predicate
:=
  (fun a => Is_true (andb a true))
.

Theorem thm_exists_basics : (ex basic_predicate).
Proof.
  pose (witness := true).
  refine (ex_intro basic_predicate witness _).
    simpl.
    exact I.
Qed.

The code as is produces the following error:

Error:
Illegal application (Non-functional construction):
The _expression_
 "ex_intro basic_predicate witness"
of type "exists x, ?P x"
cannot be applied to the term
 "?y" : "?T"

I don't actually understand why Mike expects ex_intro to take 3 arguments. From what I understand it should take 2 arguments or even 1.

Can someone point out what's wrong here?

Thanks,

Hussain

On Thu, Apr 28, 2016 at 12:19 AM, Hussain Sobhy <hussain.sob7y AT gmail.com> wrote:

Thanks Gabriel for the clarification. This is very useful.

Regards,

Hussain

On Wed, Apr 27, 2016 at 11:41 PM, Gabriel Scherer <gabriel.scherer AT gmail.com> wrote:

The difference in behavior comes from implicit arguments. Formally
or_introl or or_introl each take three arguments: the propositions A
and B, and the constructor parameter.

  Check (@or_introl True False I)

The syntax @or_introl lets me use the or_introl identifier with no
implicit argument at all.

In the book, or_introl and or_introl are considered to have their two
first parameters implicit. The failure that you show comes from the
fact that, on your machine, the parameters are not implicit. So
(or_introl) expects a proposition as first parameter, not a proof of
that proposition.

You can make the code pass unchanged by setting the following options before it:

  Set Implicit Arguments.
  Set Contextual Implicit.

  Inductive or (A B:Prop) : Prop :=
  | or_introl : A -> A \/ B
  | or_intror : B -> A \/ B
  where "A \/ B" := (or A B) : type_scope.

You will find documentation on implicit arguments in the manual,
  https://coq.inria.fr/refman/Reference-Manual004.html#Implicit%20Arguments

Note that the explicit arguments that you get depend on whether you
use the "or" type defined in the standard library, or if you redefine
your own as you show in your email. If you use the standard one, you
get the setting for implicit arguments that was decided in the
standard library code, and the example proofs work unchanged. You only
need those options if you redefine your own "or" type as you show in
your email, so that the implicit arguments are chosen in a way similar
to what the standard library does.

Another option is to manually set the implicit arguments of the
constructors, instead of a general setting

  Inductive or (A B:Prop) : Prop :=
  | or_introl : A -> A \/ B
  | or_intror : B -> A \/ B
  where "A \/ B" := (or A B) : type_scope.

  Arguments or_introl [A B] _.
  Arguments or_intror [A B] _.

On Wed, Apr 27, 2016 at 6:08 PM, Hussain Sobhy <hussain.sob7y AT gmail.com> wrote:
> Hello,
>
> I was going through Mike Nahas's tutorial
> (https://coq.inria.fr/tutorial-nahas) and I came across two examples which I
> can't get working on CoqIde.
>
> Inductive or (A B:Prop) : Prop :=
>   | or_introl : A -> A \/ B
>   | or_intror : B -> A \/ B
> where "A \/ B" := (or A B) : type_scope.
>
>
> First Example:
>
> Theorem left_or : (forall A B : Prop, A -> A \/ B).
> Proof.
>   intros A B.
>   intros proof_of_A.
>   pose (proof_of_A_or_B := or_introl proof_of_A : A \/ B).
>   exact proof_of_A_or_B.
> Qed.
>
> Error:
> In environment
> A, B : Prop
> proof_of_A : A
> The term "proof_of_A" has type "A"
> while it is expected to have type
> "Prop".
>
> Second Example:
>
> Theorem right_or : (forall A B : Prop, B -> A \/ B).
> Proof.
>   intros A B.
>   intros proof_of_B.
>   refine (or_intror _).
>     exact proof_of_B.
> Qed.
>
> Error:
> In environment
> A, B : Prop
> proof_of_B : B
> The term "or_intror ?P" has type
>  "forall B0 : Prop, B0 -> ?P \/ B0"
> while it is expected to have type
> "A \/ B".
>
> Is it due to the fact that the tutorial used an old version of Coq or is
> there something fundamentally wrong here?
>
> Thanks,
> Hussain