The Coq mailing list

[Eric Jaeger <eric.jaeger AT ssi.gouv.fr>]

(* Hi all,

Since a few weeks I've been trying to develop tacticals for Coq (mapping
on hypotheses, if you remember). I've been rather astonished by the
complexity not to develop tactics, but to understand the exact behaviour
(mixing side effect, backtracking, etc.). I've also been unable to
discover how to mix tactic invocations and values in tactics (to give an
example, I was expecting to count hypotheses by recursion with revert as
long as there was an hypothesis, before returning the current value of
the counter for an empty proof context, but this does not appear to be
possible).

Here is some feedback - except for the comments, it is rather short. You
may find some of the tactics and tactical interesting, but I also expect
comments for possible improvements. I may have missed standard features
of Coq that would have helped me; if it is the case, please let me know.

First of all, a pretty easy definition to get the type of an expression
without having to rely on "type of" tactic. This may on some occasion
simplify the writing of tactics... *)

Definition typeof(T:Type)(t:T) := T.
Implicit Arguments typeof [T].

(* Then a tactic that counts hypotheses. "count hyps as H1 H2" will
create "H1:=n:nat" and "H2:H1=n" where n is the number of hypotheses *)

Ltac count_hyps_ inb ieq :=
 let rec c_ n := match goal with
                 | [ H:_|-_ ] => revert H; c_ (S n); intro H
                 | _ => pose (inb:=n); assert (ieq:inb=n); [ apply
refl_equal | ]
                 end
 in c_ 0.

Tactic Notation "count" "hyps" "as" ident(I1) ident (I2) := count_hyps_
I1 I2.

(* When trying to develop a mapping tactical, executing a given tactic
on all hypotheses, various approach can be attempted. Lets consider a
first one.

In a context "Hm Hm-1 ... H2 H1", it invokes "T Hm", ... "T H2", "T H1".
It is always successful and not stopping if a "tac H" fails (at level
0). Note that "T" can even delete hypotheses, but this may fail
because of dependencies; "T" can also create hypotheses without causing
"map_hyp_" to loop, but this may cause renaming of pre-existing
hypotheses. *)

Ltac map_hyp_ T :=
 match goal with
 | [ H':_|-_ ] => first [ revert H'; map_hyp_ T; let H'':=fresh H' in
(intro H''; try (T H''))
                        | fail 1 "Unexpected failure of map_hyp_ at" H' ]
 | _ => idtac
 end.

Tactic Notation "exec" tactic(T) "on" "all" "hyps"  := map_hyp_ ltac:(T).

(* There are two problems with this approach, however:
- "T" should not insert head hypotheses in the goal (e.g. using
generalize) because it will cause problem when re-introducing them
- "T" should not have reference to other hypotheses (as in "fun X=>idtac
X H") because these may have been reverted during recursion. *)

(* Another approach to solve these problem is to work by copy.

In a context "Hm Hm-1 ... H2 H1", it creates "H:=H(n)" before invoking
"T H(n)". It is then easy to use this approach to develop application of
a tactic on a hypothesis referred to by its number, and mapping. *)

Ltac copy_nth_as_ n Hc :=
 match goal with
 | [ H:_|-_ ] => match n with
                 | 0 => fail 2 "Hypothesis 0 does not exist for
copy_nth_as_"
                 | 1 => pose (Hc:=H)
                 | S ?n' => revert H; copy_nth_as_ n' Hc; let H' :=
fresh H in intro H'
                 end
 | _ => fail 1 "Not enough hypotheses for copy_nth_as_"
 end.

Tactic Notation "copy" "hyp" constr(E) "as" ident(H) := copy_nth_as_ E H.

(* Of course, if you want to clear or destruct an hypothesis, this may
not be very interesting to work with a copy. *)

(* Therefore, trying to solve all the problems and have a tactical to
apply a tactic to a given hypothesis referred to by its number, here is
our final proposal. The idea is to first use recursion with "revert" to
browse all the proof context, but to save this context in a dedicated
structure. Once the right hypothesis is found, we record its identifier
in a parameter of the tactical, then use the saved context to restore
hypotheses. Finally, we can invoke the tactic on the recorded identifier *)

Inductive _context_ :=
| _ctx_nil_ : _context_
| _ctx_cns_ : forall (T:Type), T->_context_->_context_.

Ltac _ctx_mem_ T t c :=
 match c with
 | _ctx_nil_ => false
 | _ctx_cns_ ?T' ?t' ?c' => match T with
                            | T' => match t with t' => true | _ =>
_ctx_mem_ T t c' end
                            | _ => _ctx_mem_ T t c'
                            end
 end.

Ltac build_context_ acc :=
 match goal with
 | [ H:?T|-_ ] => match _ctx_mem_ T H acc with false => build_context_
(_ctx_cns_ T H acc) end
 | _ => acc
 end.
(* Note that we browse all hypotheses using backtracking, but that to
avoid to use the tactic fail (not compatible with this tactic returning
a value) backtracking is caused by incomplete pattern matching *)

Ltac get_nth_ n :=
 let ctx := build_context_ _ctx_nil_ in
 let rec gn_ n c :=
  match c with
  | _ctx_cns_ ?t' ?h' ?c' => match n with
                             | 1 => h'
                             | S ?n' => gn_ n' c'
                             end
  end
 in gn_ n ctx.

Tactic Notation "exec" tactic(T) "on" "hyp" constr(E) := let H :=
get_nth_ E in T H.

(* Here is an illustration of what it can do *)

Theorem test_get_nth_:forall (na nb:nat), na=nb->forall
(bc:bool)(nd:nat), na<=nd->True.
Proof.
 intros.

 exec (fun X=>let T1 := type of na in
              let T6 := type of H0 in
              let TX := type of X in idtac X ":" TX "remembering" T1
"and" T6) on hyp 3.
 (* An illustration of how this tactic preserve the whole context *)

 exec (fun X=>pose (nb':=X)) on hyp 2.
 (* It is possible to create new hypotheses *)

 exec (fun X=>revert X) on hyp 4.
 (* It is possible to remove hypotheses and modify the goal *)
 intros _.

 exec (fun X=>clear X) on hyp 3.
 (* It is finally possible to clear hypotheses *)

 apply I.
Qed.

(* It is then pretty easy to develop various forms of mappings or other
tacticals.

I've a question however. There are ways in coq to use numbers instead of
identifiers, e.g. for parameters in "apply le_trans with (2:=...)" or
"pattern ... at 3".

The tactics given here provide have a similar feature for hypotheses:
"get_nth_ n" returns the name of the nth hypothesis.

Is it a feature of Coq I'm not aware of? That is, I would like for
example to be able to write "destruct 3" or "rewrite 4".

  Best Regards, Eric *)