CODEWITHSUNDEEP
functional-programmingcoq
Shuzheng
Shuzheng

Reputation: 14018

How to replace hypotheses `0 < d` with `S d'` in Coq?

How to replace hypotheses 0 < d with S d' in Coq?

In Coq, I've the annoying hypotheses that 0 < d, which I need to replace to apply euclid_div_succ_d_theorem to prove euclid_div_theorem as a corollary.

How can I somehow convert the assumptions into the proper form to apply the theorem?

Theorem euclid_div_theorem :
  forall d : nat,
    0 < d -> 
    forall n : nat,
    exists q r : nat,
      n = q * d + r /\ r < d.

Theorem euclid_div_succ_d_theorem :
  forall d : nat,
  forall n : nat,
  exists q r : nat,
    n = q * (S d) + r /\ r < (S d).

Upvotes: 3

Views: 97

Answers (1)

Anton Trunov
Anton Trunov

Reputation: 15424

Using the standard lemmas from the Arith module you can change 0 < d into exists m, d = S m, which (after destruction) gives you the desired result.

Require Import Arith.

Theorem euclid_div_theorem : forall d : nat,
    0 < d -> forall n : nat, exists q r : nat, n = q * d + r /\ r < d.
Proof.
  intros d H n.
  apply Nat.lt_neq, Nat.neq_sym, Nat.neq_0_r in H.
  destruct H; rewrite H.
  apply euclid_div_succ_d_theorem.
Qed.

Here is how I did it:

Search (exists _, _ = S _). gives us the last lemma (it's easier to go backwards from your goal here, imho):

Nat.neq_0_r: forall n : nat, n <> 0 <-> (exists m : nat, n = S m)

This means we need to infer d <> 0 from 0 < d, so again Search (_ < _ -> _ <> _). yields:

Nat.lt_neq: forall n m : nat, n < m -> n <> m

Now it's easy to see that we need to swap the lhs and rhs of the inequality, so I did Search (?x <> ?y -> ?y <> ?x).:

Nat.neq_sym: forall n m : nat, n <> m -> m <> n

I could've also used a more universal lemma:

not_eq_sym: forall (A : Type) (x y : A), x <> y -> y <> x

It'd give us the same result.

There is, however, a less tedious way of proving the lemma -- you can always use destruct d. and prove it by cases:

  intros d H n.
  destruct d.
  - inversion H.   (* H is a contradiction now: `0 < 0` *)
  - apply euclid_div_succ_d_theorem.

Upvotes: 2

Related Questions