coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Alexandre Pilkiewicz <alexandre.pilkiewicz AT polytechnique.org>
- To: Thomas Braibant <thomas.braibant AT gmail.com>
- Cc: Victor Porton <porton AT narod.ru>, coq-club AT inria.fr
- Subject: Re: [Coq-Club] Why backtick notation is needed?
- Date: Fri, 4 Nov 2011 14:09:47 -0400
The ` tells to "generalize" every free variable found between the two
parenthesis
Say you have a property on types, let's say that they are comparable:
Parameter Comparable: Type -> Prop.
Then you may want to define the min of two comparable value. The
`authorizes you to say
Definition min_comp `(Comparable A) (a b:A): A := ...
It is equivalent to
Definition min_comp A (Comparable0: Comparable A) (a b:A): A := ...
The A is automatically generalized, and a arbitrary name is given to
the property "Comparable A". (you need to declare A as generalizable:
Generalizable Variables A.)
So what's the point? Well, it's usefull for typeclasses !
Class Comparable A :=
{compare: A -> A -> bool}.
Definition fst_comp `(Comparable A) (a b:A):A :=
if compare a b then a else b.
Now, you may want to have the type A (and the Type Class witness)
maximally inserted. Just write
Definition fst_comp `{Comparable A} (a b:A):A :=
if compare a b then a else b.
And you'll be able to write things like "map2 fst_comp l1 l2" for exemple.
Cheers
Alexandre
2011/11/4 Thomas Braibant
<thomas.braibant AT gmail.com>:
> The back-tick is related to type-classes, not to implicit arguments.
> In your example, you do not deal with implicit arguments. Check the
> following exceprt: there, id2 has an implicit argument, while id1 does
> not have one (which requires to give this argument by hand, while it
> can be inferred from the context).
>
> Definition id (A : Type) (x : A) := A. Definition id2 {A : Type} (x : A) :=
> A.
> Check id2 1. Check id 1. (* fails *)
> Check id nat 1. (* succeeds *)
>
> thomas
>
>
>
> On Fri, Nov 4, 2011 at 6:48 PM, Victor Porton
>Â <porton AT narod.ru>
> wrote:
>> I installed Coq 8.3.
>>
>> The following:
>>
>> <<<
>> Definition id `(x : nat) : nat := x.
>> Print id.
>>
>> Definition id2 (x : nat) : nat := x.
>> Print id2.
>>
>> Definition v := id O.
>> Definition v2 := id2 O.
>>
>> Print v.
>> Print v2.
>>>>>
>>
>> Produces the output:
>>
>> <<<
>> id = fun x : nat => x
>> : nat -> nat
>>
>> Argument scope is [nat_scope]
>> id2 = fun x : nat => x
>> : nat -> nat
>>
>> Argument scope is [nat_scope]
>> v = id 0
>> : nat
>> v2 = id2 0
>> : nat
>>>>>
>>
>> You see that types of id and id2 are identical.
>>
>> Moreover not only id but also id2 works with an implicit argument.
>>
>> What is the point to use backtick, if it work implicitly even without it?
>>
>> --
>> Victor Porton - http://portonvictor.org
>>
>
>
- [Coq-Club] Why backtick notation is needed?, Victor Porton
- Re: [Coq-Club] Why backtick notation is needed?,
Thomas Braibant
- Re: [Coq-Club] Why backtick notation is needed?,
Victor Porton
- Re: [Coq-Club] Why backtick notation is needed?, Alexandre Pilkiewicz
- Re: [Coq-Club] Why backtick notation is needed?, Alexandre Pilkiewicz
- Re: [Coq-Club] Why backtick notation is needed?,
Victor Porton
- Re: [Coq-Club] Why backtick notation is needed?, Alexandre Pilkiewicz
- Re: [Coq-Club] Why backtick notation is needed?,
Victor Porton
- Re: [Coq-Club] Why backtick notation is needed?,
Victor Porton
- Re: [Coq-Club] Why backtick notation is needed?,
Thomas Braibant
Archive powered by MhonArc 2.6.16.