The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 07/08/2016 01:31 PM, Jonathan Leivent wrote:
> 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

Attached is a cleaner version that uses typeclasses for finding sub 
eqdecs.  It doesn't have that horrid combine_subgoals hack, but is quite 
a bit slower in Fin3_eqdec as a result of not combining all those 
subgoals and instead just allowing typeclass search to resolve each 
independently.

-- 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.

(*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_eqdec := shelve.
(*Use typeclasses to search for existing eqdec instances:*)
Ltac handle_sub_eqdec := try typeclasses eauto; default_handle_sub_eqdec.

(*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|handle_sub_eqdec]
    | H : @eq (@ex _ _) _ _ |- _ =>
      apply Eqdep_dec.inj_right_pair in H; [subst|handle_sub_eqdec]
    | 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 term 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;
  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 that aren't found via
handle_sub_eqdec:*)
Ltac decide_equality :=
  try unshelve (start_eqdec;do_next_eqdec;handle_sub_eqdec).

Existing Class sumbool.
Hint Mode sumbool + + : typeclass_instances.

(*** Examples:*)

Require Import Arith.
Existing Instance Nat.eq_dec.

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

Instance 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).

Instance Fin3_eqdec : forall n f1 f2 (a b : Fin3 n f1 f2), {a=b}+{a<>b}.
Proof.
  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).

Hint Extern 5 ({?a = ?b}+{?a <> ?b}) => (*handle UIP solutions of eq_dec*)
  intros; left; apply Eqdep_dec.UIP_dec : typeclass_instances.

Instance Finx_eqdec : forall n (a b : Finx n), {a=b}+{a<>b}.
Proof.
  decide_equality.
Qed.
Print Assumptions Finx_eqdec.