coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Valentin Robert <valentin.robert.42 AT gmail.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Ideal eliminator for { l : list T & length l = n}
- Date: Fri, 21 Feb 2020 18:03:46 +0100
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=valentin.robert.42 AT gmail.com; spf=Pass smtp.mailfrom=valentin.robert.42 AT gmail.com; spf=None smtp.helo=postmaster AT mail-ot1-f48.google.com
- Ironport-phdr: 9a23:b71gvx+f/urXzv9uRHKM819IXTAuvvDOBiVQ1KB41eocTK2v8tzYMVDF4r011RmVBNmdu64P2raempujcFJDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmTWwbalxIRi5ogncssYbipZ+J6gszRfEvnRHd+NKyG1yOFmdhQz85sC+/J5i9yRfpfcs/NNeXKv5Yqo1U6VWACwpPG4p6sLrswLDTRaU6XsHTmoWiBtIDBPb4xz8Q5z8rzH1tut52CmdIM32UbU5Uims4qt3VBPljjoMOjgk+2/Vl8NwlrpWrx2vpxN9w4DaboKbOudgcKzBZt4VX3ZNU9xLWiBdHo+xbY0CBPcBM+ZCqIn9okMDohSkCgmoGuzvzCNIhn7w3aYnz+ohFhrJ0xI6H9ISrX/Zq8v1O70WUe+ryqnI0TTDb/VM1Tfn74jHaQ4uoeuQXb5qfsfd11IiFwzAjlqKqIzlOymZ2fgKs2ie9udtU/+khW0/qwxpvDSj2sMhhpPKi48V0FzI6zh1zJovKdC3S0N2Z8OvHoFKuCGALYR2R9svQ2F2tyY+zb0LoZu7czILyJQj3hLfbOCHf5WR7hLtW+ucIi10hH1ieLK4iBay9VavxvfgWcmz1VZGtitFkt/SuXARzxHf9NSLR/9n8kqi2TuDzR7f5vxYLUwumqfWKIYtwrsqmZoStUTDEDX2mELzjKKOaEUr4Oyo5PrhYrX6p5+cMZV4ihv5Mqs1hMO/G/g4PhIBUmSF4um827jj8lf4QLVOlPE5jq7ZsJXCKcQBuqG5GxNV0pok6xunEzim180YkWAbI1JBZRKIlJPkO0rOIfD9FfewmU6gkDZtx/DcP73uGI/BLnbZkOSpQbEo4ElFjQE30Np35pROC7hHLuigdFX2sYnmBxs0NRC1xa7dD99wzJ9WDXyGBqKfLKLU90WP7O81P6/QPqcavT/8L74u4Pu43ixxokMUYaT8hchfU3u/BPkzexzEM0qpuc8IFCIxhiR7TOHujwffAztaZnL3WL5loz9nWMSpCoDMQo3ri7uEjn/iT89mI1teA1XJKk/GMoCNWvMCciWXe5YznTkNVLznQIgkh0j36F3KjoF/J++RwRU28Ir53YEsteLWnBA2szdzCpbF3g==
Very nice, indeed fixing `n`, unlike in the more general `Vector.caseS`, makes the problems I had go away!
- Valentin
On Fri, 21 Feb 2020 at 17:34, Daniel Schepler <dschepler AT gmail.com> wrote:
On Fri, Feb 21, 2020 at 2:42 AM Valentin Robert
<valentin.robert.42 AT gmail.com> wrote:
> Or I have to painfully roll my own inversion:
>
> Goal forall T (P : Vector.t T 2 -> Type) v, P v.
> move => T P v.
> pose goal :=
> (
> fun n v =>
> match n as n' return Vector.t T n' -> Type with
> | 2 => P
> | _ => fun _ => True
> end v
> ).
What if instead, you rolled the basic vectorS_inv and vector0_inv
once, and then used those as building blocks? e.g.
Definition vectorS_inv {X:Type} {n:nat} :
forall P : Vector.t X (S n) -> Type,
(forall (h : X) (t : Vector.t X n), P (Vector.cons _ h _ t)) ->
forall v : Vector.t X (S n), P v.
Admitted.
Definition vector0_inv {X:Type} :
forall P : Vector.t X O -> Type,
P (Vector.nil _) -> forall v : Vector.t X O, P v.
Admitted.
Goal forall {X:Type} (P : Vector.t X 2 -> Type),
(forall a b : X, P (Vector.cons _ a _ (Vector.cons _ b _ (Vector.nil _)))) ->
forall v : Vector.t X 2, P v.
intros X P f v. destruct v as [a0 v'] using @vectorS_inv.
destruct v' as [b0 v''] using @vectorS_inv.
inversion v'' using @vector0_inv. apply f.
Defined.
--
Daniel Schepler
- [Coq-Club] Ideal eliminator for { l : list T & length l = n}, Talia Ringer, 02/21/2020
- Re: [Coq-Club] Ideal eliminator for { l : list T & length l = n}, Jason Gross, 02/21/2020
- Re: [Coq-Club] Ideal eliminator for { l : list T & length l = n}, Valentin Robert, 02/21/2020
- Re: [Coq-Club] Ideal eliminator for { l : list T & length l = n}, Daniel Schepler, 02/21/2020
- Re: [Coq-Club] Ideal eliminator for { l : list T & length l = n}, Valentin Robert, 02/21/2020
- Re: [Coq-Club] Ideal eliminator for { l : list T & length l = n}, Talia Ringer, 02/21/2020
- Re: [Coq-Club] Ideal eliminator for { l : list T & length l = n}, Talia Ringer, 02/21/2020
- Re: [Coq-Club] Ideal eliminator for { l : list T & length l = n}, Dominique Larchey-Wendling, 02/21/2020
- Re: [Coq-Club] Ideal eliminator for { l : list T & length l = n}, Emilio Jesús Gallego Arias, 02/22/2020
- Re: [Coq-Club] Ideal eliminator for { l : list T & length l = n}, Jason Gross, 02/22/2020
- Re: [Coq-Club] Ideal eliminator for { l : list T & length l = n}, Hugo Herbelin, 02/22/2020
- Re: [Coq-Club] Ideal eliminator for { l : list T & length l = n}, Arthur Azevedo de Amorim, 02/22/2020
- Re: [Coq-Club] Ideal eliminator for { l : list T & length l = n}, Jason Gross, 02/22/2020
- Re: [Coq-Club] Ideal eliminator for { l : list T & length l = n}, Hugo Herbelin, 02/22/2020
- Re: [Coq-Club] Ideal eliminator for { l : list T & length l = n}, Talia Ringer, 02/23/2020
- Re: [Coq-Club] Ideal eliminator for { l : list T & length l = n}, Talia Ringer, 02/21/2020
- Re: [Coq-Club] Ideal eliminator for { l : list T & length l = n}, Valentin Robert, 02/21/2020
- Re: [Coq-Club] Ideal eliminator for { l : list T & length l = n}, Daniel Schepler, 02/21/2020
- Re: [Coq-Club] Ideal eliminator for { l : list T & length l = n}, Valentin Robert, 02/21/2020
- Re: [Coq-Club] Ideal eliminator for { l : list T & length l = n}, Jason Gross, 02/21/2020
Archive powered by MHonArc 2.6.18.