The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 07/08/2016 12:14 PM, Jonathan Leivent wrote:
> On 07/08/2016 11:56 AM, Matthieu Sozeau wrote:
> > Hi Jonathan,
> >
> > ...
> > Both fin_eqdec and Fin3_eqdec are closed under the global context, as 
> > they
> > are using instances of decidable equality for nat and fin.
> > This eqdec_proof tactic is not able to handle your Finx example 
> > currently
> > though, it's also work in progress. How did you implement your tactic?
>
> I am close to having a standalone demo version that uses the standard 
> Eqdec_dep.  So I will send this to you as soon I have it, which should 
> be quite soon.  It is not very big or complex.

Attached...

-- Jonathan

(*** A version of decide equality without axioms.*)

(*Uses 8.5pl1 and may depend on fixes for things like congruence added
afterwards - hence it may not work on an earlier build.*)

Require Coq.Logic.Eqdep_dec.

Global Set Injection On Proofs.

Ltac revert_all := repeat lazymatch goal with H : _ |- _ => revert H end.

(*Do induction on H, but make sure the induction is helpful - a quick check is
that its first subgoal is not the same as the original goal.  Note that this
cheats a little in that it relies on progress not detecting the change to the
shelf. *)
Ltac helpful_induction H := unshelve (progress (induction H; [|shelve..])).

Ltac default_handle_sub_deceq := clear;revert_all;shelve.
Ltac handle_sub_deceq := default_handle_sub_deceq.

(*Do injections, making sure they aren't the useless variety that just repeats
the injecting hyp (which would cause an infinite loop) - also handle any
sigma-based equalities that are either from some previous injection or from
the pose_sigmaT mechanism below.*)
Ltac do_injections :=
  repeat
    match goal with
    | H : @eq (@sigT _ _) _ _ |- _ =>
      apply Eqdep_dec.inj_pair2_eq_dec in H; [subst|default_handle_sub_deceq]
    | H : @eq (@ex _ _) _ _ |- _ =>
      apply Eqdep_dec.inj_right_pair in H; [subst|default_handle_sub_deceq]
    | H : _ = _ |- _ =>
      let H' := fresh in
      let tH := type of H in
      injection H as H';
      let tH' := type of H' in
      (*if the result of the injection is no different, avoid it:*)
      tryif constr_eq tH tH' then fail else idtac;
      subst
    end.

(*Given a hyp equality, which we really really want to subst, at least on the
conclusion, try a bunch of tactics to make it subst:*)
Ltac force_subst H :=
  lazymatch type of H with
  | ?X = ?Y =>
    first [subst X
          |subst Y
          |change X with Y
          |change Y with X
          |replace X with Y by congruence
          |replace Y with X by congruence
          |rewrite !H
          |rewrite <- !H
          |fail 1 "Cannot substitute" X "with" Y
          ]
  end.

(*Given an eqdec conclusion, walk through the args of the compared term and
try to discharge each via a sub eqdec:*)
Ltac do_next_eqdec :=
  idtac; (*avoid early eval*)
  let rec f pair :=
      lazymatch pair with
      | (?A, ?A) => left; reflexivity
      | (?A ?X, ?A ?Y) => (*pick off first differnce*)
        let H := fresh in
        assert ({X=Y}+{X<>Y}) as [H|H];
        [(*sub eqdec*)
          try (*check if there is an induction hypothesis that can be applied:*)
            match goal with IH :_ |- _ => apply IH; assumption end
        |(*H:X=Y case*)tryif force_subst H then do_next_eqdec else idtac
        |(*H:X<>Y case*)try (right; contradict H; do_injections; congruence)]
      | (?F _, ?G _) => f (F, G)
      | _ => try (right; discriminate)
      end in
  lazymatch goal with
  | |- ({?X=?Y}+{_}) => f (X, Y)
  | _ => fail
  end.

(*Given a term (or type), return its head symbol and arity:*)
Ltac head_arity term :=
  let rec f x :=
      lazymatch x with
      | (?F ?A, ?N) => f (F, S N)
      | _ => x
      end in
  f (term, 0).

(*Pose a nested sigT for term as H.  This is the basis of the mechanism that
allows destruct on H when it is very dependently intertwined with the goal.
Why this works: this nested sigT container can wrap a copy of term, but do so
such that its type is not "co-dependent" with term - meaning that none of
term's type indexes are part of this nested sigT's type.  That's important
because an equality between two such nested sigTs (both wrapping term), with
just one side of the equality unfolded to expose the existTs, will maintain a
validly typed equality between the destructing term and its generalized
counterpart in the conclusion, even though some of term's type indexes change
due to the destruct. *)
Ltac pose_sigT term H :=
  let rec f h n :=
      lazymatch n with
      | 0 => h
      | S ?m =>
        let a := fresh in
        constr:(sigT (fun a => ltac:(let h' := constr:(h a) in
                                  let r := f h' m in exact r)))
      end in
  let type := type of term in
  let ha := head_arity type in
  let s := lazymatch ha with (?h, ?n) => f h n end in
  simple refine (let H := _ : s in _); [repeat eapply existT; exact term|].

(*Kind of like "generalize_eqs X; destruct X", but using a nested sigT
equality instead of a JMeq to maintain the equivalence between the destructee
and the generalized copy of it in the conclusion:*)
Ltac depdestruct H :=
  let s := fresh in
  pose_sigT H s;
  generalize (eq_refl s); (*conclusion now is "s=s -> ..."*)
  unfold s at 1; (*unfold only one side of the above s=s equality to make it's H visible*)
  generalize H; (*all H's visible in the goal are generalized away from being dependent on H*)
  destruct H;
  subst s;
  (*intro just the 2 generalizations above - the first should come back as H
  if all dependencies on H were removed via the generalization (to force that,
  first do "revert dependent H; intro H" prior to calling depdestruct)*)
  intros ? ?;
  subst;
  do_injections.

(*start an eqdec proof - trying both the non-dependent and dependent mechanisms:*)
Ltac start_eqdec :=
  intros; clear;
  lazymatch goal with
    |- ({?a=?b}+{_}) =>
    generalize a, b;
    let X := fresh in
    intro X;
    tryif helpful_induction X
    then (let Y := fresh in intro Y; first[destruct Y | depdestruct Y])
    else fail
  end.

(*Do just one level of eqdep, leaving any sub-eqdeps:*)
Ltac decide_one_equality :=
  try unshelve (start_eqdec;do_next_eqdec;handle_sub_deceq).

(*Because the above can generate many like-typed eqdec subgoals, instead of
recursively dealing with each separately, we would like to combine them to
leave fewer.  The following is a generic global tactic to combine like-typed
subgoals together.  This is quite a bit of a hack, but it isn't really
necessary either.  Somewhat unfortunately, the refines used to name and rename
goals will also induce typeclass search - and so any subgoals that can get
filled that way will be, even before all like subgoals can be combined.  This
can get fixed by wrapping the subgoals with something before calling refine on
them < TODO.*)
Ltac combine_subgoals :=
  let ng := numgoals in
  do ng (try refine ?[_Combine_subgoals];
         try solve[intros;apply ?_Combine_subgoals];
         refine _;
         cycle 1).

(*Putting it all together.  Note that each invocation of decide_one_equality
does only one "level" of eqdec, leaving behind any sub-eqdec goals, which then
get combined by combine_subgoals (or solved as typeclass instances).  Hence,
"repeat decide_one_equality" is a complete solution.  However, note that the
repeat tactical loses global focus, so not all resulting like-typed sub-eqdecs
will get combined across subgoals if repeat is used.  Also, note that we can't
"sort" the subgoals so that the absolute minimum of sub-eqdecs are done.
Unfortunately, because we want the iteration to give up when it can't make
progress, and there is no current way to do this without losing global focus
(see bug 3878 for lengthy discussion), that's the best we can currently do.*)
Ltac decide_equality := repeat (decide_one_equality; combine_subgoals).

(*** Examples:*)

Inductive Fin : nat -> Set :=
| F1 : forall n : nat, Fin (S n)
| FS : forall n : nat, Fin n -> Fin (S n).

Lemma Fin_eqdec: forall n (a b : Fin n), {a=b}+{a<>b}.
Proof.
  decide_equality.
Qed.
Print Assumptions Fin_eqdec.

Inductive Fin3 : forall n (f1 f2 : Fin n), Set :=
| F31 : forall m (f1 f2 : Fin m), (f1 = f2) -> Fin3 (S m) (FS _ f1) (FS _ f2)
| F3S : forall m (f1 f2 : Fin m), Fin3 m f1 f2 -> Fin3 (S m) (FS _ f1) (FS _ f2).

Lemma Fin3_eqdec : forall n f1 f2 (a b : Fin3 n f1 f2), {a=b}+{a<>b}.
Proof.
  (*Just to make a point about the usefullness of combine_subgoals, the
  following leaves 23 sub-eqdecs, but only 2 distinct ones:*)
  decide_one_equality.
  all:combine_subgoals.
  Restart.
  decide_equality.
Qed.
Print Assumptions Fin3_eqdec.

Inductive Finx(n : nat) : Set :=
| Fx1(i : nat)(e : n = S i)
| FxS(i : nat)(f : Finx i)(e : n = S i).

Ltac handle_sub_deceq ::=
  (*Add ability to handle UIP cases - this could have been built-in, but doing
  it this way illustrates another way becides typeclasses to ofload eqdep
  subgoals:*)
  try (intros; left; apply Eqdep_dec.UIP_dec);
  default_handle_sub_deceq.

Lemma Finx_eqdec : forall n (a b : Finx n), {a=b}+{a<>b}.
Proof.
  (*Note that without the UIP addition above, this would leave an unsolved
  eqdec corresponding to FxS e field:*)
  decide_equality.
Qed.
Print Assumptions Finx_eqdec.