Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Getting "computing" proof terms with dependent types / reduction of matches with single pattern

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Getting "computing" proof terms with dependent types / reduction of matches with single pattern


Chronological Thread 
  • From: Guillaume Melquiond <guillaume.melquiond AT inria.fr>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Getting "computing" proof terms with dependent types / reduction of matches with single pattern
  • Date: Wed, 7 Sep 2016 15:56:21 +0200

On 07/09/2016 15:38, Soegtrop, Michael wrote:
> Dear Guillaume,
>
> thanks a lot, your example gives some interesting insight into how match
> works. So if I have nat = bool, I can convince match to accept 1 as a bool:
>
> Definition foo2 (H : nat = bool) : bool :=
> match H in (_ = t) return t with
> | eq_refl => 1
> end.
>
> But I wonder how this really works. I can see that an "in" clause is used
> to bind a variable to a part of the match argument type and this is used in
> a "return" clause. But how does Coq know that it should use the equality to
> relate this to the actual return type? Is there a rule that if the match
> argument is an equality of types, it can be used to unify the declared and
> actual return type?

There is absolutely nothing specific about equality. This is just the
way "match" works in Coq's theory. The sentence "in (foo t) return (bar
t)" means that, whenever the matched argument is of type (foo t), the
result of the "match" is of type (bar t). Coq just checks that this is
true for all the branches of the "match"; if so, it assumes that it is
also true for the "match" itself.

In your definition, "eq_refl" has type (_ = nat) and 1 is of type nat,
so the "match" is well-typed. It works fine because the day H will have
an actual value, it will necessary be (@eq_refl nat). And since it
cannot have an actual value, there is no contradiction.

> Coming back to my issues with computations with dependent types: how about
> reducing such matches, in case the types are unifiable, as in the example I
> have shown where the types are "t bool (0+1)" and "t bool 1". This should
> be quite common in computations with concrete values of dependent types,
> e.g. vectors of known length.

I am no specialist, but I believe people tend to consider a different
approach. Any term is flagged as being closed under the global context
or not. If you are matching against such a closed term, then the
reduction you suggest is applied even if the term is opaque. (Obviously,
H in the example above is not closed, so the reduction cannot be applied.)

I don't know if anyone ever tried this approach for Coq or if it has
some issues in the context of Coq.

Best regards,

Guillaume



Archive powered by MHonArc 2.6.18.

Top of Page