The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

I haven't tried this, but do any of

Theorem pf_3_le_14 : 3 <= 14. ... Qed.

Theorem ttt m n (p : m <= n) : (pred m) <= n. ... Qed.

Eval simpl in @ttt _ _ pf_3_le_14.

Eval unfold pred in @ttt _ _ pf_3_le_14.

Eval cbv beta iota zeta delta [pred] in @ttt _ _ pf_3_le_14.

Check (@ttt _ _ pf_3_le_14 : 2 <= 14).

work?

Alternatively, you can try unfolding pred manually, and state your theorem as either

Theorem ttt m n (p : S m <= n) : m <= n.

or

Theorem ttt m n (p : m <= n)) : match m with | O => O | S m' => m' end <= n.

(Coq might simplify the match for you automatically in the second case.)

-Jason

On Mon, Jul 1, 2013 at 10:56 AM, Ilmārs Cīrulis <ilmars.cirulis AT gmail.com> wrote:

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?