The Coq mailing list

["Gyesik Lee" <gyesik.lee AT aist.go.jp>]

Thanks for the answers.

It is great to see Coq's ability to handle the dependent equalities.
I might look into the paper by Conor McBride to understand the inner
workings of the new tactics which is already done implicitly by Adam's
answer.

Gyesik


PS. One comment more:
In Widonws version,

Require Import Equality

works, but not

Require Import Program.Equality.


On Fri, Aug 1, 2008 at 7:37 AM, Matthieu Sozeau 
<sozeau AT lri.fr>
 wrote:
>
> Le 31 juil. 08 à 14:50, Adam Chlipala a écrit :
>
>> Gyesik Lee wrote:
>>>
>>> in case of representing the semantics of a language, it is sometimes
>>> necessary to have the uniqueness of the term constructions. But since
>>> terms are usually of dependent types, it is not so simple to prove the
>>> uniqueness because of heterogeneous equality or dependency.
>>>
>>> Here is one simple example.
>>>
>>> Inductive P : nat -> bool -> Set :=
>>> T : forall n, P n true.
>>>
>>> Goal forall (n : nat) (x : P n true), x = T n.
>>>
>>> (* one would try *)
>>> intros n x.
>>> destruct x.
>>>
>>> But the tactic destruct fails with the warning (using Coq 8.2beta3)
>>>
>>> Error: Abstracting over the terms "n", "b" and "x" leads to a term
>>> "fun (n : nat) (b : bool) (x : P n b) => x = T n" which is ill-typed.
>>>
>>> Maybe one has to use first the tactic of the following form
>>>
>>> pattern n at nums, true at nums , x at nums
>>>
>>> to get a well-typed application term, and then use "destruct". But I
>>> don't understand exactly the process.
>>>
>>
>> [destruct] is only going to work well when _all_ of the arguments of the
>> type family you're destructing are variables.  You might also have to run
>> [change] on some of the variables to get their types to match those in the
>> definition of the type family.  These restrictions arise from the CIC 
>> typing
>> rule for [match], which is the building block for [destruct].
>>
>> I think that the general problem you're pointing out could be used to
>> solve the higher-order unification problem, so we know it must be
>> undecidable.  Tactics like [dependent inversion] make heuristic attempts at
>> solving it in limited cases.
>>
>> It's hard to give a short description of how to solve this problem in
>> practice.  The best I can do is show how to solve your specific example
>> using [JMeq].  (Keep in mind that this involves introducing an axiom, as
>> seen in the manual page for the [JMeq] module.)
>
> Hello,
>
> The same can now be done using
> <<
> Require Import Program.Equality.
>
> Inductive P : nat -> bool -> Set :=
> T : forall n, P n true.
>
> Goal forall (n : nat) (x : P n true), x = T n.
> intros n x.
> dependent destruction x. reflexivity.
> Qed.
>>>
>
> The [dependent destruction] tactic essentially does as variant of the
> construction Adam has shown automatically.
> It is actually a combination of tactics that can be used and understood
> separately (e.g. to do dependent
> induction-inversion using the same basic idea), and is defined in
> Program.Equality. It also uses [JMeq] if necessary,
> that is if the object you destruct appears in the goal. The reference for
> this technique is the "Elimination with a
> motive" paper by Conor McBride. The tactic's also documented in the
> reference manual.
> --
> Matthieu Sozeau
> http://www.lri.fr/~sozeau
>
> --------------------------------------------------------
> Bug reports: http://logical.futurs.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>         http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>