coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Daniel Schepler <dschepler AT gmail.com>
- To: Gert Smolka <smolka AT ps.uni-saarland.de>
- Cc: coq-club AT inria.fr, Adam Chlipala <adam AT chlipala.net>
- Subject: Re: [Coq-Club] Inductive family of finite types
- Date: Tue, 28 Jun 2011 14:37:03 -0700
On Tue, Jun 28, 2011 at 9:28 AM, Gert Smolka <smolka AT ps.uni-saarland.de> wrote:
How about constructing an inversion function in a form which is easy to feed into the inversion tactic?
Definition Fin_inversion_aux (n:nat) (x:Fin n) :
match n as n0 return (Fin n0 -> Type) with
| 0 => fun _ => Empty_set
| S m => fun x:Fin (S m) => forall (P:Fin (S m) -> Type)
(P0:P (FinO m)) (PS: forall y:Fin m, P (FinS m y)),
P x
end x :=
match x with
| FinO n0 => fun P P0 PS => P0
| FinS n0 x0 => fun P P0 PS => PS x0
end.
Definition Fin_inversionS (n:nat) (P:Fin (S n) -> Type)
(P0: P (FinO n)) (PS: forall x:Fin n, P (FinS n x))
(x:Fin (S n)) : P x :=
Fin_inversion_aux (S n) x P P0 PS.
Definition Fin_inversion0 (P:Fin 0 -> Type) (x:Fin 0) : P x :=
match (Fin_inversion_aux 0 x) with
end.
Lemma Fin1: forall k:Fin 1, k = FinO 0.
Proof.
inversion k using Fin_inversionS.
trivial.
inversion x using Fin_inversion0.
Qed.
--
Daniel
Thanks Adam, you made my day.
So the trick is to formulate the inversion
lemma with a match so that it type checks.
How about constructing an inversion function in a form which is easy to feed into the inversion tactic?
Definition Fin_inversion_aux (n:nat) (x:Fin n) :
match n as n0 return (Fin n0 -> Type) with
| 0 => fun _ => Empty_set
| S m => fun x:Fin (S m) => forall (P:Fin (S m) -> Type)
(P0:P (FinO m)) (PS: forall y:Fin m, P (FinS m y)),
P x
end x :=
match x with
| FinO n0 => fun P P0 PS => P0
| FinS n0 x0 => fun P P0 PS => PS x0
end.
Definition Fin_inversionS (n:nat) (P:Fin (S n) -> Type)
(P0: P (FinO n)) (PS: forall x:Fin n, P (FinS n x))
(x:Fin (S n)) : P x :=
Fin_inversion_aux (S n) x P P0 PS.
Definition Fin_inversion0 (P:Fin 0 -> Type) (x:Fin 0) : P x :=
match (Fin_inversion_aux 0 x) with
end.
Lemma Fin1: forall k:Fin 1, k = FinO 0.
Proof.
inversion k using Fin_inversionS.
trivial.
inversion x using Fin_inversion0.
Qed.
--
Daniel
- [Coq-Club] Inductive family of finite types, Gert Smolka
- Re: [Coq-Club] Inductive family of finite types, Adam Chlipala
- <Possible follow-ups>
- Re: [Coq-Club] Inductive family of finite types,
Paolo Herms
- Re: [Coq-Club] Inductive family of finite types,
Gert Smolka
- Re: [Coq-Club] Inductive family of finite types,
Adam Chlipala
- Re: [Coq-Club] Inductive family of finite types,
Gert Smolka
- Re: [Coq-Club] Inductive family of finite types, Daniel Schepler
- Re: [Coq-Club] Inductive family of finite types,
Gert Smolka
- Re: [Coq-Club] Inductive family of finite types,
Adam Chlipala
- Re: [Coq-Club] Inductive family of finite types,
Gert Smolka
- Re: [Coq-Club] Inductive family of finite types, ahrens
Archive powered by MhonArc 2.6.16.