The Coq mailing list

[Florian Haftmann <florian.haftmann AT informatik.tu-muenchen.de>]

Dear all,

for demonstration purpose I am currently tinkering around with Cezar
(current coq release 8.2) using some simple propositions.
At one stage I run into a problem of understanding;  I have the
following proof fragment (see below for the full example):

      focus on (S q + s = n). escape.
        rewrite n_Sr. simpl. rewrite qsr. reflexivity.
      return. end focus.

According to my understanding of Cezar this could also be written as

      thus (S q + s = n)
        using rewrite n_Sr; simpl; rewrite qsr; reflexivity.

However this is rejected as insufficient justification.

What am I missing?

Any help appreciated,
        Florian

--

Require Import Arith.

Theorem le_Sm_n_pred:
  forall m n: nat, S m <= n -> { q : nat | S q = n }.
proof.
  let m: nat, n: nat.
  per cases on n.
    suppose it is 0.
      assume (S m <= 0).
      hence thesis by (le_Sn_O m).
    suppose it is (S q).
      thus thesis using exists q; reflexivity.
  end cases.
end proof. Qed.

Theorem exists_minus:
  forall m n: nat, m <= n -> { q : nat | m + q = n }.
proof.
  let m: nat.
  per induction on m.
    suppose it is 0.
      let n: nat.
      thus thesis using simpl; exists n; reflexivity.
    suppose it is (S q) and hyp: thesis for q.
      let n: nat.
      assume Sq_n: (S q <= n).
      then ex_r: {r : nat | S r = n} by (le_Sm_n_pred q n).
      consider r such that (S r = n) from ex_r.
      then n_Sr: (n = S r).
      then (S q <= S r) by Sq_n.
      then (q <= r).
      then ex_s: {s : nat | q + s = r} by hyp.
      consider s such that qsr: (q + s = r) from ex_s.
      (* the following works *)
      focus on (S q + s = n). escape.
        rewrite n_Sr. simpl. rewrite qsr. reflexivity.
      return. end focus.
      (* this more concise version refuses to work:
      thus (S q + s = n)
        using rewrite n_Sr; simpl; rewrite qsr; reflexivity.
      *)
    end induction.
end proof. Qed.

-- 

Home:
http://wwwbroy.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature