CODEWITHSUNDEEP
coqcoq-tactic
Carl Patenaude Poulin
Carl Patenaude Poulin

Reputation: 6589

Coq: apply the f_equal tactic only when f is an inductive constructor

The f_equal tactic is unconditionally useful for equality proofs involving inductive constructors. a :: s = a' :: s would be such a goal, reducing to a = a'.

Using it with arbitrary functions is a different story. 4 mod 2 = 2 mod 2 would reduce to 4 = 2, which is clearly absurd.

I'm wondering if there's a way to automatically apply f_equal (or similar) only in cases where it doesn't lose information, e.g. inductive constructors.

Upvotes: 2

Views: 1510

Answers (2)

Zimm i48
Zimm i48

Reputation: 3081

Here is an alternative, non-hackish way, using Ltac2 (with help from Ltac2's author Pierre-Marie Pédrot):

From Ltac2 Require Import Ltac2.

Ltac2 is_constructor c := match Constr.Unsafe.kind c with
| Constr.Unsafe.Constructor _ _ => true
| _ => false
end.

Ltac2 not_a_constructor f :=
  let msg :=
    Message.concat (Message.of_constr f) (Message.of_string " is not a constructor")
  in
  Control.zero (Tactic_failure (Some msg)).

Ltac2 dest_app c := match Constr.Unsafe.kind c with
| Constr.Unsafe.App f args => (f, args)
| _ => (c, Ltac2.Array.make 0 constr:(Type))
end.

Ltac2 f_equal_ind () :=
  lazy_match! goal with
  | [ |- ?lhs = _ ] =>
    let (f, _) := dest_app lhs in
    match is_constructor f with
    | true => f_equal
    | false => Control.zero (not_a_constructor f)
    end
  | [ |- _ ] =>
    Control.zero (Tactic_failure (Some (Message.of_string "Goal is not an equality")))
  end.

Ltac2 Notation "f_equal_ind" := f_equal_ind ().

(* Tests *)

Require Import List.
Import ListNotations.
Require Import Arith.

Goal forall (a a' : nat) s, a :: s = a' :: s.
intros.
f_equal_ind. (* a = a' *)
Abort.

Goal True.
Fail f_equal_ind.
(* 
The command has indeed failed with message:
Uncaught Ltac2 exception: Tactic_failure (Some (message:(Goal is not an equality)))
*)
Abort.

Goal 1 mod 2 = 3 mod 4.
Fail f_equal_ind.
(*
The command has indeed failed with message:
Uncaught Ltac2 exception: Tactic_failure (Some (message:(Nat.modulo is not a constructor)))
*)
Abort.

You can find Ltac2 documentation at https://coq.github.io/doc/master/refman/proof-engine/ltac2.html. It will be released with Coq 8.11, but sources compatible with the previous versions of Coq can be found in the various branches of https://github.com/coq/ltac2/branches/all.

Upvotes: 3

Zimm i48
Zimm i48

Reputation: 3081

Here is a way to specialize f_equal to inductive constructors only with a bit of Ltac:

Ltac f_equal_ind :=
  match goal with
  | [ |- ?G ] =>
    tryif
      (tryif assert (~ G); [ injection |]
       then fail else idtac)
    then
      fail "Not an inductive constructor"
    else
      f_equal
  end.

Require Import List.
Import ListNotations.

Goal forall (a a' : nat) s, a :: s = a' :: s.
intros.
f_equal_ind.
Abort.

Require Import Arith.

Goal 4 mod 2 = 2 mod 2.
Fail f_equal_ind.

(* The command has indeed failed with message:
   In nested Ltac calls to "f_equal_ind" and "f_equal_ind", last call failed.
   Tactic failure: Not an inductive constructor. *)

I must say the result is particularly involved and I wouldn't be surprised if there was a simpler way. My idea is to test whether we are working on a primitive equality using injection which expects a negated primitive equality. The nested tryif is because the assert (~ G); [ injection |] part is just for testing but we don't want to keep the subgoals that this created.

Upvotes: 2

Related Questions