The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 02/11/2016 09:12 AM, Saulo Araujo wrote:
> Hi Jonathan,
>
> Thanks a lot for suggesting another technique. The resulting code is quite
> pleasant and, at least to me, has one of the best signal to noise ratio :)
>
> I never saw the character @ used as an operator. I looked in the Coq
> reference manual and if, I understood it correctly, it disables the
> inference of implicit parameters. Could you confirm if I understood it
> correctly?
>
> Sincerely,
> Saulo

Yes, the "@" operator (which isn't technically an operator - it is 
instead built into the Gallina syntax as a identifier prefix character) 
makes all args explicit.  However, it isn't really needed here, as the 
following get definition shows:

Fixpoint get E n (t: Sequence E n) (ds: List Digit n): E.
Proof.
refine(
  match t with
  | SequenceLeaf e0 e1 _ =>
      match ds with
      | ListLeaf D0 _ => e0
      | ListLeaf D1 _ => e1
      | ListNode _ _ _ => _
      end
  | SequenceNode s0 s1 _ =>
      match ds with
      | ListLeaf _ _ => _
      | ListNode d _ _ =>
          match d with
          | D0 => get E _ s0 _
          | D1 => get E _ s1 _
          end
      end
  end
).
all:congruence.
Defined.

-- Jonathan


> On Wed, Feb 10, 2016 at 9:50 PM, Jonathan Leivent 
> <jonikelee AT gmail.com>
> wrote:
>
> > There is another alternative.  The type indexes can be omitted in favor of
> > extra equality fields.  Doing this enables the use of basic matches in the
> > refine, as in the following rewriting of your example.  No convoy patterns
> > are needed.  I don't know why this technique isn't mentioned more
> > frequently.
> >
> >
> > Set Implicit Arguments.
> >
> > Section Sequence.
> >
> > Variable E: Set.
> >
> > Inductive Sequence(n : nat) : Set :=
> >    | SequenceLeaf: E -> E -> n=0 -> Sequence n
> >    | SequenceNode: forall m, Sequence m -> Sequence m -> n = S m ->
> > Sequence n.
> >
> > Inductive List(n : nat) : Set :=
> >    | ListLeaf: E -> n=0 -> List n
> >    | ListNode: forall m, E -> List m -> n = S m -> List n.
> >
> > End Sequence.
> >
> > Inductive Digit :=
> >    | D0
> >    | D1.
> >
> > Fixpoint get E n (t: Sequence E n) (ds: List Digit n): E.
> > Proof.
> > refine(
> >    match t with
> >    | SequenceLeaf e0 e1 e =>
> >        match ds with
> >        | ListLeaf D0 _ => e0
> >        | ListLeaf D1 _ => e1
> >        | @ListNode _ _ y _ _ e2 => _
> >        end
> >    | @SequenceNode _ _ x s0 s1 _ =>
> >        match ds with
> >        | ListLeaf _ e0 => _
> >        | @ListNode _ _ y d ds' _ =>
> >            match d with
> >            | D0 => get E x s0 _
> >            | D1 => get E x s1 _
> >            end
> >        end
> >    end
> > ).
> > all:congruence.
> > Defined.
> >
> > -- Jonathan