The Coq mailing list

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

On my machine, the code in your email works fine if I *prefix* it by
the following:

Set Implicit Arguments.

Definition Is_true (b : bool) : Prop :=
  match b with
    | true => True
    | false => False
  end.

On Thu, Apr 28, 2016 at 3:40 PM, Hussain Sobhy 
<hussain.sob7y AT gmail.com>
 wrote:
> Thanks for the clarification.
>
> But is the code in the tutorial correct? I can't seem to get it working in
> an implicit or explicit setting.
>
> On Thu, Apr 28, 2016 at 7:04 PM, Gabriel Scherer 
> <gabriel.scherer AT gmail.com>
> wrote:
>>
>> 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
>> >>
>> >>
>> >
>
>