The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

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.