The Coq mailing list

[Ilmārs Cīrulis <ilmars.cirulis AT gmail.com>]

Apologies to Pierre Casteran for accidentally answering to his email.

---------- Forwarded message ----------
From: Ilmārs Cīrulis <ilmars.cirulis AT gmail.com>
Date: Tue, Jul 2, 2013 at 11:36 AM
Subject: Re: [Coq-Club] Problems when writing function from proof to proof.
To: Pierre Casteran <pierre.casteran AT labri.fr>

Here's example of what I want to make.

Theorem ttt (m n:nat) (p: m<=n): (pred m) <= n.
Proof. destruct m. assumption. simpl. apply le_S_n. inversion p; auto. Qed.

Theorem _3_14: 3<=14. repeat constructor. Qed.
Eval simpl in (ttt 3 14 _3_14).

Fixpoint example (m n: nat) (p: m<=n): list nat :=
match m with
| O => nil
| S m' => cons m (example m' n (ttt m n p))
end.

Function example has error that I want to fix:

In environment
example : forall m n : nat, m <= n -> list nat
m : nat
n : nat
p : m <= n
m' : nat
The term "ttt m n p" has type "pred m <= n" while it is expected to have type
"m' <= n".

On Mon, Jul 1, 2013 at 7:42 PM, Pierre Casteran <pierre.casteran AT labri.fr> wrote:

Hi,

  I don't understand what you want exactly to get.
  By Coq's typing rules, a proof of pred 3 <= 14 is ***already*** a proof of 2 <=14.

Theorem ttt (m n:nat) (p: m<=n): (pred m) <= n.
Proof.
 destruct m. assumption. simpl. apply le_S_n. inversion p; auto.
Qed.

Require Import Arith.

Example E1 : 3 <= 14.
auto with arith. Qed.

Check ttt _ _ E1 : 2 <= 14.



Pierre

Quoting Ilmārs Cīrulis <ilmars.cirulis AT gmail.com>:

I tried to make function (?) that's transforming proof of m<=n to proof of
(pred m)<=n.

My try was:
Theorem ttt (m n:nat) (p: m<=n): (pred m) <= n.
Proof.
 destruct m. assumption. simpl. apply le_S_n. inversion p; auto.
Qed.

But it always gives proof of (pred m)<=n. For example, proof of 3<=14 is
transformed to (pred 3)<=14. I don't know how to simplify it to 2<=14
(using the same function).

Is it possible?