The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

The lemma you want is

Lemma Fix_eq : forall x:A, Fix x = F (fun (y:A) (p:R y x) => Fix y).

in Coq.Init.Wf.  You should never unfold Fix unless you're running the full computation of the function.  (You will have to unfold test, though.)

On Mon, Oct 26, 2020, 17:05 Mallku Ernesto Soldevila Raffa <mallkuernesto AT gmail.com> wrote:

Hi everyone!

I'm trying to understand how to prove properties about well-founded

recursions defined through the Fix combinator. As a simple (artificial) example,

I'm including the code of a function test : nat -> nat, that should return 0,

always.

When trying to prove the simpl_prop lemma below, after unfolding and

simplification, I'm unable to use the inductive hypothesis since it is expressed in

terms of a call to test, while in the goal I have a term involving Fix_f.

Are there some lemmas in the standard library that allow me to reason about

these definitions without resorting to unfold/simpl?

The code:

Require Import
        Arith.Wf_nat.

Definition test (n1 : nat) : nat.
  refine (Fix
         lt_wf
         (* possible dependent range type of the function that we are
            building *)
         (fun n : nat => nat)
         (* the function body *)
         (fun (n1 : nat)
            (test2 : forall (n2 : nat),
                     (lt n2 n1) -> nat) =>
             match n1 as n1' return n1 = n1' -> nat with
             | 0        => fun eqp : _             => 0
             | (S n1'') => fun eqp : n1 = (S n1'') => (test2 n1'' _)
             end
               eq_refl) n1).
rewrite eqp.
unfold lt.
apply le_n.
Defined.

Lemma simpl_prop : forall n, (test n) = 0.
Proof.
  apply (well_founded_induction lt_wf).
  intros.
  destruct x.
  + reflexivity.
  + unfold test.
    unfold Fix.
    unfold Fix_F.
    destruct (lt_wf (S x)).

Thanks in advance!

Best,

Mallku