The Coq mailing list

[Mallku Ernesto Soldevila Raffa <mallkuernesto AT gmail.com>]

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