The Coq mailing list

[Vincent Archambault-Bouffard <archambault.v AT gmail.com>]

Thank you !

It’s clever to package all arguments in a tuple and use Function instead of Program.

Vincent

On Jun 16, 2016, at 2:41 AM, Pierre Casteran <pierre.casteran AT labri.fr> wrote:

Hi,

 I think this problem was already discussed in coq-club :
 Please look at
http://coq-club.inria.narkive.com/c2SDnwrl/executability-and-fixpoint-equation-of-a-program-fixpoint-definition


By the way, The Recdef library provides tools for proving your ko theorem.

I'm not sure, but I think that a definition by Function works only with
one decreasing argument, so I defined an auxiliary function.


Function compose' (p : Foo * Foo)
        {measure (fun p => foo_size (fst p) + foo_size (snd p))}

                                                : Foo :=
 match p with
 | (CInt 0, _) => snd p
 | (CInt (S n1), CInt n2) => CInt (S n1 + n2)
 | (CInt (S n1), CFoo s3) => compose' (CInt n1, s3)
 | (CFoo s, _) => CFoo (compose' (s, snd p))
 end
.

intros;simpl;auto with arith.
auto with arith.
Defined.

Definition compose s1 s2 := compose' (s1,s2).

Then, using the automatically generated induction principle compose'_ind, you get a rewriting lemma.

Lemma compose'_rw :
  forall p : Foo * Foo,
    compose' p =
    match p with
      | (CInt 0, _) => snd p
      | (CInt (S n1), CInt n2) => CInt (S n1 + n2)
      | (CInt (S n1), CFoo s3) => compose' (CInt n1, s3)
      | (CFoo s, _) => CFoo (compose' (s, snd p))
    end.


Then, your theorem becomes trivial to prove.

Theorem ko : forall n1 s1,
   compose (CInt (S n1)) (CFoo s1) = compose (CInt n1) s1.
Proof.
 unfold compose; intros; now rewrite compose'_rw.
Qed.

Pierre



Le 16/06/2016 07:02, Vincent Archambault-Bouffard a écrit :

Require Import Coq.Program.Wf.
Require Import Omega.
Inductive Foo : Set :=
| CFoo : Foo -> Foo
| CInt : nat -> Foo
.

(* This will serve as the measure to convince coq that compose
terminates. *)
Fixpoint foo_size (s : Foo) : nat :=
  match s with
    | CFoo s' => 1 + foo_size s'
    | CInt _ => 1
  end.

Program Fixpoint compose (s1 s2 : Foo)
        {measure (foo_size s1 + foo_size s2)} : Foo :=
  match s1, s2 with
  | CInt 0, _ => s2
  | CInt (S n1), CInt n2 => CInt (S n1 + n2)
  | CInt (S n1), CFoo s3 => compose (CInt n1) s3
  | CFoo s, _ => CFoo (compose s s2)
  end
.
Theorem ko : forall n1 s1,
    compose (CInt (S n1)) (CFoo s1) = compose (CInt n1) s1.
Proof.