coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Gyesik Lee <gslee AT ropas.snu.ac.kr>
- To: Roman Beslik <beroal AT ukr.net>
- Cc: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Indexed Types Pattern Matching Problem
- Date: Mon, 22 Mar 2010 17:01:27 +0900
- Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:in-reply-to:references:date :x-google-sender-auth:message-id:subject:from:to:cc:content-type; b=q8Afwas2GaO8oqWxHr5HPKcu+czTXyOE6D5wOfMhFgQDfA4R6FJVRpYEuQ70F6b+vz /lT+fWhU6ndVkJ5EocN++aFhRHFeRi94ee+NZuMW8+TUsVViUhGzWwtT17UPsr06eDwk ZutNXq7x7COpllUjLIWqSbQZ8LOfaV4YKLimE=
2010/3/20 Roman Beslik
<beroal AT ukr.net>:
> First, Coq thinks that structural argument is "a". Because of "match x", I
> suppose that structural argument is "x", so write it explicitly: "fix to_T
> (a : Rep) (x : Interpret RT a) {struct x} : ...". Then you must call "to_T"
> with a subterm of "x". That subterm is of type "Interpret RT Rec". "to_T"
> may not receive an argument of such a type, so you can not call "to_T".
> Recursion is impossible.
Using {struct x} doesn't help.
> And it does not make sense to me. What do you suppose "to_T" to do?
It should reproduce the set T from its interpretation (Interpret RT RT).
(RT is a kind of a representative of T)
=======
Having seen that the problem setting seems to be not trivial to
handle, let me ask questions one by one.
First, I would like to know why the proof mode in [to_T] won't close
where I use "refine (fix ...)" style to use induction on the
well-founded relation based on the structurally-smaller-than-relation.
(I am aware of the danger of using "fix" and using Coq 8.2pl1)
Inductive Rep : Type :=
| Plus : Rep -> Rep -> Rep
| Rec : Rep
| Const : Type -> Rep.
Inductive Interpret (r : Rep) : Rep -> Type :=
| inl : forall a b, Interpret r a -> Interpret r (Plus a b)
| inr : forall a b, Interpret r b -> Interpret r (Plus a b)
| rec : Interpret r r -> Interpret r Rec
| const : forall a, a -> Interpret r (Const a).
Inductive T :=
| A : nat -> T
| B : T -> T.
Definition RT := Plus (Const nat) Rec.
Definition to_T (a : Rep) (x : Interpret RT a) : (a = RT) -> T.
refine (fix to_T (a : Rep) (x : Interpret RT a) {struct x}: (a = RT) -> T :=
match x with
| inl a b _ => _
| inr a b _ => _
| rec _ => _
| const a _ => _
end
); intros; try discriminate.
(* only the case [a = Plus l r] remains.*)
(* first case: [l = (Const nat)] *)
inversion H.
subst a0.
(* to get [i = const nat X] for some X *)
inversion i.
(* use the X *)
exact (A X).
(* second case: [r = Rec] *)
inversion H.
subst b.
(* to get [i = rec X for some X of type (Interpret RT RT) *)
inversion i.
(* apply to_T to this X which is structrually smaller than x. *)
exact (to_T RT X (refl_equal RT)).
(* the proof is finished, but termination check failed although X is
obviously structurally smaller than x. *)
Defined.
- [Coq-Club] Indexed Types Pattern Matching Problem, Gyesik Lee
- Re: [Coq-Club] Indexed Types Pattern Matching Problem,
Roman Beslik
- Re: [Coq-Club] Indexed Types Pattern Matching Problem,
Gyesik Lee
- Re: [Coq-Club] Indexed Types Pattern Matching Problem,
Roman Beslik
- Re: [Coq-Club] Indexed Types Pattern Matching Problem, Gyesik Lee
- Re: [Coq-Club] Indexed Types Pattern Matching Problem,
Roman Beslik
- Message not available
- Re: [Coq-Club] Indexed Types Pattern Matching Problem, Roman Beslik
- Re: [Coq-Club] Indexed Types Pattern Matching Problem, Gyesik Lee
- Message not available
- Re: [Coq-Club] Indexed Types Pattern Matching Problem,
Roman Beslik
- Re: [Coq-Club] Indexed Types Pattern Matching Problem, Gyesik Lee
- Re: [Coq-Club] Indexed Types Pattern Matching Problem,
Roman Beslik
- Re: [Coq-Club] Indexed Types Pattern Matching Problem,
Gyesik Lee
- Re: [Coq-Club] Indexed Types Pattern Matching Problem,
Roman Beslik
- Re: [Coq-Club] Indexed Types Pattern Matching Problem, Adam Chlipala
Archive powered by MhonArc 2.6.16.