The Coq mailing list

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

The arguments of the constructor may also include the parameters of
the type itself.

Check @ex_intro.
> ex_intro : forall (A : Type) (P : A -> Prop) (x : A), P x -> exists x, P x

A can be easily inferred as it is completely determined by the types
of P and x. On the contrary, P is harder to infer from the other
parameters (and I don't know whether Coq can reason about how to
extract if from (exists x, P x). With the common default settings of
implicit arguments, A will be considered implicit and P, x and (_ : P
x) will not.

Note that the syntax (A := A) in the ex declaration code you used only
makes sense when the A parameter is implicit.

On Thu, Apr 28, 2016 at 1:33 PM, Hussain Sobhy 
<hussain.sob7y AT gmail.com>
 wrote:
> 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
>>
>>
>