coq-club AT inria.fr
Subject: The Coq mailing list
List archive
Re: [Coq-Club] using Ltac to retrieve the name of an induction principle from the type
Chronological Thread
- From: Pierre Courtieu <pierre.courtieu AT gmail.com>
- To: Coq Club <coq-club AT inria.fr>
- Cc: MAGAUD Nicolas <magaud AT unistra.fr>
- Subject: Re: [Coq-Club] using Ltac to retrieve the name of an induction principle from the type
- Date: Sat, 25 Mar 2017 02:12:50 +0100
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=pierre.courtieu AT gmail.com; spf=Pass smtp.mailfrom=pierre.courtieu AT gmail.com; spf=None smtp.helo=postmaster AT mail-wm0-f48.google.com
- Ironport-phdr: 9a23:asQlGhHELLoG+IU23vFuCp1GYnF86YWxBRYc798ds5kLTJ78oM+wAkXT6L1XgUPTWs2DsrQf2raQ6/iocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbQhFgDWwbaluIBmqsA7cqtQYjYx+J6gr1xDHuGFIe+NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S6dYDCk9PGAu+MLrrxjDQhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VC+85Kl3VhDnlCYHNyY48G7JjMxwkLlbqw+lqxBm3oLYfJ2ZOP94c6jAf90VWHBBU95TWCxPAo2yYYgBAfcfM+lEtITyvUcCoAGkCAWwGO/iyDlFjWL2060g1OQhFBnL0hYhH90QqnTUtsv6P7oMXOCy0anI1ynDb/JI1jfg9YPFdQghofCSUrJqa8re11MjGB/CjlWNs4zlIzKV2foQs2WA4OpgUPigi28jqw1rvjevwcIsh5DPi4kIyV7E7T10zYQ6KNGiVUJ3f96pHIFTui2ELYd7TcAvTmd1sygg0LIGo4S0fC0SxZQn2RHfb/uHfpCN4h35VeaRJS50hXxgeL6jnhqy/0etx+7mWsm711ZKqSVFkt3SuXwXyxPT7c2HRuN8/kenxzmPyxje5+NLLEwuiKbXNZ4szqQzm5YNq0jOESz7lF3zjKCMd0Uk/uao6/7gYrXjvpKcL450hR/kMqQ0hMOzG/g3Mg8TX2iB5eS81aPs/VDiTbVFi/05iKjZsJTAKcsHoa65BhdZ0pw/5BanEzemzNMYkGEbI1JCYRKLlpTmO1XTIP/jFvq/mFStkDJzx//cJLHhA5PNLmLCkLj7Z7p95VRcm0IPyoV04IscIbUcKrqnUUjo8dfcExURMgquwu+hBs8rha0EXmfaOq6UKrnf+XSP+/gzIuSRLNsNuTvnMfVj7Pnzl2M4lEI1cqyg3J9RY3e9SKc1a36FaGbh149SWVwBuRAzGamz0AWP
Hi Nicolas, here a small hack to do this, not sure this is really robust but hope this helps.
The idea is that "the associated induction principle." means "the constant you will find in your proof term when you do "induction"".
The ltac below performs a "induction" on a dummy proof and extract the head constant.
(* find the hd term of an application *)
Ltac hd_of_app t :=
match t with
| (?f _) => hd_of_app f
| _ => t
end.
Ltac find_rec h :=
let typ := type of h in
let X := constr:(fun x:typ => (ltac:(induction h;exact I)):True) in
let app := eval lazy beta in (X h) in
let hd := hd_of_app app in
hd.
(* example: *)
Inductive t:=A|B|C.
Parameter P : t -> nat -> Prop.
Lemma l : forall a n, P a n.
Proof.
intros.
let schem := find_rec a in apply schem.
Undo.
let schem := find_rec n in apply schem.
Best,
P.
Le ven. 24 mars 2017 à 14:34, Nicolas Magaud <magaud AT unistra.fr> a écrit :
Hello,
I would like to write a Ltac tactic which, from the type of a variable (obtained using the function "type of”), retrieves and applies the associated induction principle.
If _x is of type nat, it applies nat_rect; if _x is of type t, it applies t_rect (see example below).
So far, I do it using Ltac pattern-matching, which is weird as “t” does not belong to an inductive type and my Ltac function has to be extended manually each time I handle a new inductive type.
I would prefer something like (type of _x)^”_rect” which appends the appropriate extension to the tacexpr1 returned by "type of”.
Is there any way to do that using only Ltac (i.e. without writing any .ml or .ml4 files) ?
Nicolas Magaud
------
Inductive t:=A|B|C.
Ltac use_pattern _x:= pattern _x;
match goal with |- (?f _x) =>
let t:= (type of _x) in
match t with
| nat => apply nat_rect
| t => apply t_rect
end end.
Parameter P : t -> nat -> Prop.
Lemma l : forall a n, P a n.
Proof.
intros.
use_pattern a.
Undo.
use_pattern n.
- [Coq-Club] using Ltac to retrieve the name of an induction principle from the type, Nicolas Magaud, 03/24/2017
- Re: [Coq-Club] using Ltac to retrieve the name of an induction principle from the type, Beta Ziliani, 03/24/2017
- Re: [Coq-Club] using Ltac to retrieve the name of an induction principle from the type, Pierre Courtieu, 03/25/2017
Archive powered by MHonArc 2.6.18.