The Coq mailing list

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

Hello,

I am relatively new to Coq and I have a hard time proving something that is true by definition.

Here is a (simplified) working example :

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.

    ??????

This is true by definition (3rd pattern in the match in the definition of compose)

Yet I cannot convince Coq that it is true

I tried reflexivity, destruct n1, s1, induction. I just don’t know how to translate “by definition” in Coq. Usually reflexivity does the job but not this time. 

Thank you for your help.

Vincent