Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] "as <_ or unused variable in the return type> in ... return ..." pattern matching

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] "as <_ or unused variable in the return type> in ... return ..." pattern matching


Chronological Thread 
  • From: Jason Gross <jasongross9 AT gmail.com>
  • To: coq-club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] "as <_ or unused variable in the return type> in ... return ..." pattern matching
  • Date: Fri, 21 Mar 2014 03:49:38 -0400

Coq seems to be interpreting "match r in ..." as "match r as r in ...".  The following version of vredex works:

Definition vredex n o r (r' := r) : VarRedex n o r :=
  match r
  in redex _ t return match t with Var _ => VarRedex n o r' | _ => unit end
  with ARedex _ _ | LRedex _ _ _ | RRedex _ _ _ | BRedex _ _ => tt end.

Perhaps someone else can elaborate on why this is the case.

-Jason


On Fri, Mar 21, 2014 at 5:13 AM, AUGER Cédric <sedrikov AT gmail.com> wrote:
Hi all, today I found a situation where I had to use a "match … as _
in … return …" instead of a "match … as <some name used in the returned
type> in … return …" or a "match … in … return …".

I used to believe that "as _" was the default when not needing to bind
the pattern matched _expression_ to the result type.
Is this a new behavior or something I never noticed?
(To be honest, it is not that often that I wish the pattern matched
_expression_ not to be bound to the return type, so the current behavior
does not annoy me much. Still, I am curious of the answer.)

I use a rather old version of Coq (a trunk version from October 2012),
so things may have changed since.

(************************************************)
Fixpoint ord (n : nat) : Type :=
  match n with
  | O => Empty_set
  | S n => option (ord n)
  end.

Inductive T (n : nat) : Type :=
  | Var : ord n -> T n
  | Fun : T (S n) -> T n
  | App : T n -> T n -> T n
  .

Inductive redex (n : nat) : T n -> Type :=
  | ARedex (u : T (S n)) : redex (S n) u -> redex n (Fun n u)
  | LRedex (u v : T n) : redex n u -> redex n (App n u v)
  | RRedex (u v : T n) : redex n v -> redex n (App n u v)
  | BRedex (u : T (S n)) (v : T n) : redex n (App n (Fun n u) v)
  .

Inductive VarRedex (n : nat) (o : ord n) : redex n (Var n o) -> Type := .

Definition vredex n o r : VarRedex n o r :=
  match r as _ (*Woo, first time I have to put an underscore here*)
  in redex _ t return match t with Var _ => VarRedex n o r | _ => unit end
  with ARedex _ _ | LRedex _ _ _ | RRedex _ _ _ | BRedex _ _ => tt end.





Archive powered by MHonArc 2.6.18.

Top of Page