Merge branch 'ralf/get_head' into 'master'

add get_head tactic and use it in solve_proper_unfold

See merge request !311

CHANGELOG.md

@@ -153,6 +153,8 @@ API-breaking change is listed.
   `difference_insert`, `difference_insert_subseteq`. (by Hai Dang)
 - Tweak reduction on `gset`, so that `cbn` matches the behavior by `simpl` and
   does not unfold `gset` operations. (by Paolo G. Giarrusso, BedRock Systems)
+- Add `get_head` tactic to determine the syntactic head of a function
+  application term.
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).

tests/tactics.v

@@ -82,3 +82,10 @@ Goal ∀ mx, mx = Some 10 → is_Some mx.
 Proof. done. Qed.
 Goal ∀ mx, Some 10 = mx → is_Some mx.
 Proof. done. Qed.
+
+(** get_head tests. *)
+Lemma test_get_head (f : nat → nat → nat → nat) : True.
+Proof.
+  let f' := get_head (f 0 1 2) in unify f f'.
+  let f' := get_head f in unify f f'.
+Abort.

theories/tactics.v

@@ -238,6 +238,14 @@ Ltac mk_evar T :=
   let _ := match goal with _ => clear e end in
   e'.
 
+(** The tactic [get_head t] returns the head function [f] when [t] is of the
+shape [f a1 ... aN]. This is purely syntactic, no unification is performed. *)
+Ltac get_head e :=
+  lazymatch e with
+  | ?h _ => get_head h
+  | _    => e
+  end.
+
 (** The tactic [eunify x y] succeeds if [x] and [y] can be unified, and fails
 otherwise. If it succeeds, it will instantiate necessary evars in [x] and [y].
 
@@ -412,17 +420,12 @@ Tactic Notation "f_equiv" "/=" := csimpl in *; f_equiv.
 we proceed by repeatedly using [f_equiv]. *)
 Ltac solve_proper_unfold :=
   (* Try unfolding the head symbol, which is the one we are proving a new property about *)
-  lazymatch goal with
-  | |- ?R (?f _ _ _ _ _ _ _ _ _ _) (?f _ _ _ _ _ _ _ _ _ _) => unfold f
-  | |- ?R (?f _ _ _ _ _ _ _ _ _) (?f _ _ _ _ _ _ _ _ _) => unfold f
-  | |- ?R (?f _ _ _ _ _ _ _ _) (?f _ _ _ _ _ _ _ _) => unfold f
-  | |- ?R (?f _ _ _ _ _ _ _) (?f _ _ _ _ _ _ _) => unfold f
-  | |- ?R (?f _ _ _ _ _ _) (?f _ _ _ _ _ _) => unfold f
-  | |- ?R (?f _ _ _ _ _) (?f _ _ _ _ _) => unfold f
-  | |- ?R (?f _ _ _ _) (?f _ _ _ _) => unfold f
-  | |- ?R (?f _ _ _) (?f _ _ _) => unfold f
-  | |- ?R (?f _ _) (?f _ _) => unfold f
-  | |- ?R (?f _) (?f _) => unfold f
+  try lazymatch goal with
+  | |- ?R ?t1 ?t2 =>
+    let h1 := get_head t1 in
+    let h2 := get_head t2 in
+    unify h1 h2;
+    unfold h1
   end.
 (** [solve_proper_prepare] does some preparation work before the main
 [solve_proper] loop.  Having this as a separate tactic is useful for debugging