Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Inductive family of finite types

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Inductive family of finite types


chronological Thread 
  • 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:
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
 



Archive powered by MhonArc 2.6.16.

Top of Page