The Coq mailing list

[mukesh tiwari <mukeshtiwari.iiitm AT gmail.com>]

Hi everyone,

The only difference I see in the proof of *Fixpoint* and *Theorem* is the place of variable *t* and I am wondering if this case is very similar to [1, 2, 3]?  It appears to me that generalisation makes things complicated in this case and [1, 2, 3]. In [1], *x* is universally quantified and proof requires eq_rect_eq_dec, and in [2] proof no longer requires eq_rect_eq_dec but at the same time *x* is no longer universally quantified.

Best,

Mukesh

(* [1] and requires eq_rect_eq_dec and *x* is universally quantified *)

Lemma fin_case :
  forall n (P : Fin (S n) -> Type),
    (P (F1 _)) ->
    (forall x, P (FS _ x)) ->
    (forall x, P x).
Proof.
  intros.
  refine (match x as x' in Fin n'
                return forall pf : n' = S n,
                         eq_rect n' Fin x' (S n) pf = x ->
                         P x with
            | F1 _ => _
            | FS _ _ => _
          end eq_refl eq_refl).
  - intros.
    inversion pf.
    subst.
    rewrite <- Eqdep_dec.eq_rect_eq_dec by apply eq_nat_dec.
    auto.
  - intros.
    inversion pf.
    subst.
    rewrite <- Eqdep_dec.eq_rect_eq_dec by apply eq_nat_dec.
    auto.
Qed.


(* [2] no longer requires eq_rect_eq_dec but *x* is no longer universally quantified *)
Definition fin_case n x : 
    forall (P : Fin.t (S n) -> Type),
    P F1 -> (forall y, P (FS y)) -> P x :=
  match x as x0 in Fin.t n0
     return
       forall P,
         match n0 as n0' return (t n0' -> (t n0' -> Type) -> Type) with
           | 0 => fun _ _ => False
           | S m => fun x P => P F1 -> (forall x0, P (FS x0)) -> P x
         end x0 P
  with
    | F1 _ => fun _ H1 _ => H1
    | FS _ _ => fun _ _ HS => HS _
  end.
  
  

(** [3] The inversion principle [fin_S_inv] is more convenient than its variant
[Fin.caseS] in the standard library, as we keep the parameter [n] fixed.
In the tactic [inv_fin i] to perform dependent case analysis on [i], we
therefore do not have to generalize over the index [n] and all assumptions
depending on it. Notice that contrary to [dependent destruction], which uses
the [JMeq_eq] axiom, the tactic [inv_fin] produces axiom free proofs.*)

Definition fin_S_inv {n} (P : fin (S n) → Type)
  (H0 : P 0%fin) (HS : ∀ i, P (FS i)) (i : fin (S n)) : P i.
Proof.
  revert P H0 HS.
  refine match i with 0%fin => λ _ H0 _, H0 | FS i => λ _ _ HS, HS i end.
Defined.

[1] https://jamesrwilcox.com/dep-destruct.html

[2] https://jamesrwilcox.com/more-cardinality.html

[3] https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/stdpp/fin.v?ref_type=heads#L54

On Fri, May 3, 2024 at 7:29 AM Elias Castegren <elias.castegren AT it.uu.se> wrote:

Dear all

While investigating writing custom induction principles
I figured out that an alternative solution is to write your
theorems as Fixpoints (questions below).

For example, take this definition of a Rose tree where
the generated induction principle is unhelpful:

Inductive rose_tree (A: Type) :=
| Node (elem: A) (children: list (rose_tree A)).

Check rose_tree_ind.
(*
rose_tree_ind
     : forall (A : Type) (P : rose_tree A -> Prop),
       (forall (elem : A) (children : list (rose_tree A)),
        P (Node A elem children)) ->
       forall r : rose_tree A, P r
*)

Trying to prove for example that a convoluted identity
function is indeed an identity function fails almost
immediately:

Fixpoint rebuild (A: Type) (t: rose_tree A) :=
  match t with
  | Node _ elem children => Node A elem (map (rebuild A) children)
  end.

Theorem rebuild_id:
  forall A t,
    rebuild A t = t.
Proof.
  intros A t.
  induction t. (* No induction hypothesis generated *)
Abort.

Now, the standard solution to this is to write a custom
induction principle that recurses through the list (or something
using well-founded induction), but you can also prove the
theorem directly by formulating it as a Fixpoint:

Fixpoint rebuild_id (A: Type) (t: rose_tree A):
  rebuild A t = t.
Proof with auto.
  destruct t. simpl.
  f_equal. induction children...
  simpl. rewrite rebuild_id'.
  rewrite IHchildren...
Qed.

I was pleasantly surprised by this since I have always found
writing induction principles quite tedious, especially for larger
data types. An obvious drawback of this is that automation
tends to be very eager to use the theorem recursively too
early, creating a non-terminating proof object.

So, to my questions:

1. Is there a tactic that I can use in the proof of a regular
Theorem that turns it into a fixpoint so that I don’t have to
write the theorem statement differently? Note that writing
"Fixpoint rebuild_id: forall A t, rebuild A t = t” fails with an
uncaught exception at the moment.

2. Is there a version of auto that checks guardedness and
backtracks if it fails? What I want is something like
“try solve[auto; Guarded]”, but it seems like Guarded is a
command rather than a tactic so that they don’t compose
(also I guess solve would stop once auto solved the goal?)

Maybe there are other tricks one can employ to solve the
same problem? My goto solution is using well-founded
induction over some size measure, but it always involves
some boilerplate that would be nice to avoid.

Cheers

/Elias








När du har kontakt med oss på Uppsala universitet med e-post så innebär det att vi behandlar dina personuppgifter. För att läsa mer om hur vi gör det kan du läsa här: http://www.uu.se/om-uu/dataskydd-personuppgifter/

E-mailing Uppsala University means that we will process your personal data. For more information on how this is performed, please read here: http://www.uu.se/en/about-uu/data-protection-policy