The Coq mailing list

[Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>]

1. 
https://coq.inria.fr/doc/master/refman/proofs/writing-proofs/reasoning-inductives.html#coq:tacn.fix
used like

Lemma double : nat -> nat.
Proof. fix double 1. intros [|n];[exact 0|exact (S (S (foo n)))]. Defined.

2. the root of the proof is not visible to tactics, they only know about the 
current goals. So they cannot check guardedness.

Gaëtan Gilbert

On 03/05/2024 08:28, Elias Castegren 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