LinearTactics
Pierre Letouzey edited this page Oct 27, 2017
·
11 revisions
I tried to have a small set of tactics which clean the hypothesis they use:
- clean (removes some hypothesis and recursively all dependent hypothesis)
- purge/purge_goal (same job as clean but fails if ALL dependent hypothesis cannot be cleared, so purge_goal is a good cleaner, but also very dangerous as you can get silently rid of hypothesis)
- linear forward (an assert cleaning its hypothesis)
- linear backward (an apply cleaning its hypothesis)
See and run the last example.
(** * cleaning tactic *)
Ltac clean H :=
match H with
| ?a ?b => clean a; clean b; try clean a
| ?a _ => clean a
| _ ?b => clean b
| forall (a: ?A), ?B => clean B; clean A
| ?A -> ?B => clean B; clean A
| fun u => ?f => idtac "not tested feature"; clean f
| ?x => clean_aux x
end
with clean_aux H :=
match type of H with
| Type => try clear H
| Prop => try clear H
| ?t => try (clear H; clean t)
end.
(** this tactics fails if it cannot completely clean some hypothesis *)
Ltac purge H :=
match H with
| ?a ?b => purge a; purge b
| ?a ?b => purge b; purge a
| forall (a: ?A), ?B => purge B; purge A
| ?A -> ?B => purge B; purge A
| fun u => ?f => idtac "not tested feature"; purge f
| ?x => purge_aux x
end
with purge_aux H :=
match type of H with
| Type => clear H
| Prop => clear H
| ?t => clear H; purge t
end.
Ltac purge_goal :=
repeat
match goal with
| H: _ |- _ => purge_aux H
end.
(** * The forward and backward linear tactics *)
(** ** It performs an [assert] and [clean] all no more needed hypothesis *)
(** It uses same kind of hack as [exploit] tactic in Compcert *)
(** we don't care about induction principles generation;
we do not use the predefined "list" type constructor,
but it is cleaner not to do so, so the user cannot be
confused *)
CoInductive TacList :=
| TacListNil
| TacListCons: forall A, A -> TacList -> TacList.
Notation "'forward' x .. y 'as'" :=
(TacListCons _ x .. (TacListCons _ y TacListNil) .., true)
(x at level 0).
Notation "'backward' x .. y" :=
(TacListCons _ x .. (TacListCons _ y TacListNil) .., false)
(x at level 0, at level 0).
Ltac fwx H t l :=
match l with
| TacListNil => let h := fresh H in
assert (h := t);
clean t;
rename h into H
| TacListCons ?A ?a ?b =>
( fwx H (t a) b
|| fwx H (t _ a) b
|| fwx H (t _ _ a) b
|| fwx H (t _ _ _ a) b
|| fwx H (t _ _ _ _ a) b
|| fwx H (t _ _ _ _ _ a) b
|| fwx H (t _ _ _ _ _ _ a) b
|| fwx H (t _ _ _ _ _ _ _ a) b)
end.
(** ** The backward tactic *)
(** *** not a very smart tactic; it is a [linear forward] followed by [apply] *)
Tactic Notation "linear" constr(t) :=
(match t with
| (TacListCons ?A ?a ?l, false) => let H := fresh in
fwx H a l;
apply H; clean H
| _ => fail "Sorry, I couldn't combine the given terms"
end).
(** ** The forward tactic *)
Tactic Notation "linear" constr(t) ident(H) :=
(match t with
| (TacListCons ?A ?a ?l, true) => fwx H a l
| _ => fail "Sorry, I couldn't combine the given terms"
end).
(** * Improved now *)
(** in Coq 8.2, "easy" can be slower than auto,
so here is a patch to correct it *)
Tactic Notation "now" tactic (a) := (a; auto; easy).
Example cleaning_test:
forall (A B C D E F: Prop),
(A -> B -> C) ->
((B -> C) -> D -> E -> F) ->
(A -> E) ->
A -> D -> F.
Proof.
intros A B C D E F HABC HBCDEF HAE HA HD.
(* we will use two time A, so we need to duplicate it *)
assert (A_backup := HA).
linear forward HABC HA as HBC. (* now H and H2 do not exist anymore *)
linear forward HAE A_backup as HE.
(* now HAE and HE do not exist anymore, and neither does A *)
linear backward HBCDEF. (* now HBCDEF does not exist anymore *)
purge_goal. (* keeps all hypothesis depending on B and C *)
assumption.
clear -HD. (* clear all but D and HD *)
assumption.
easy.
(* I know this tactic is sufficient to do all the job,
but not for illustrate *)
Qed.
To the extent possible under law, the contributors of “Cocorico!, the Coq wiki” have waived all copyright and related or neighboring rights to their contributions.
By contributing to Cocorico!, the Coq wiki, you agree that you hold the copyright and you agree to license your contribution under the CC0 license or you agree that you have permission to distribute your contribution under the CC0 license.