The Coq mailing list

[Gabriel Scherer <gabriel.scherer AT gmail.com>]

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