Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Induction on evidence for the "less than" relation in coq

I am working on the proof of the following theorem Sn_le_Sm__n_le_m in IndProp.v of Software Foundations (Vol 1: Logical Foundations).

Theorem Sn_le_Sm__n_le_m : ∀n m,
  S n ≤ S m → n ≤ m.
Proof.
  intros n m HS.
  induction HS as [ | m' Hm' IHm'].
  - (* le_n *) (* Failed Here *)
  - (* le_S *) apply IHSm'.
Admitted.

where, the definition of le (i.e., ≤) is:

Inductive le : nat → nat → Prop :=
  | le_n n : le n n
  | le_S n m (H : le n m) : le n (S m).
Notation "m ≤ n" := (le m n).

Before induction HS, the context as well as the goal is as follows:

n, m : nat
HS : S n <= S m
______________________________________(1/1)
n <= m

At the point of the first bullet -, the context as well as the goal is:

n, m : nat
______________________________________(1/1)
n <= m

where we have to prove n <= m without any context, which is obviously impossible.

Why does it not generate S n = S m (and then n = m) for the le_n case in induction HS?

like image 261
hengxin Avatar asked May 24 '19 12:05

hengxin


People also ask

How to do proofs by structural induction in Coq?

Coq provides a special syntax Fixpoint/match for generic primitive recursion, and we could thus have defined directly addition as: end. Let us now show how to do proofs by structural induction. We start with easy properties of the plus function we just defined. Let us first show that n = n +0. Coq < Lemma plus_n_O : forall n : nat, n = n + 0.

Is there an induction lemma in Coq?

Recall the induction principle on naturals that Coq generates for us automatically from the Inductive declation for nat. There's nothing magic about this induction lemma: it's just another Coq lemma that requires a proof. Coq generates the proof automatically too... end.

What is an inductive relation?

ModulePlayground. Just like properties, relations can be defined inductively. One useful example is the "less than or equal to" relation on numbers that we briefly saw above. Inductivele: nat→nat→Prop:= | le_n(n: nat) : lenn | le_S(nm: nat) (H: lenm) : len(Sm).

Can you write a proof term directly in Coq?

Although tactic-based proofs are normally much easier to work with, the ability to write a proof term directly is sometimes very handy, particularly when we want Coq to do something slightly non-standard. Recall the induction principle on naturals that Coq generates for us automatically from the Inductive declation for nat.


2 Answers

The main problem here -I think- is it is impossible to prove the Theorem using induction on HS as there is no way to say something about n with only hypothesis about S n because non of the constructors of le do not change the value of n. But anyway the reason that after first bullet - there is no assumption is because calling induction has the effect of replacing all occurrences of the property argument by the values that correspond to each constructor and it doesn't help in this case since the term that gets replaced S n is not mentioned anywhere. There are some tricks to avoid this. for example you can replace n with pred(S n) as follows.

Theorem Sn_le_Sm__n_le_m : forall n m,
  S n <= S m -> n <= m.
Proof.
  intros n m HS.
  assert(Hn: n=pred (S n)). reflexivity. rewrite Hn.
  assert(Hm: m=pred (S m)). reflexivity. rewrite Hm.
  induction HS.
  - (* le_n *) apply le_n.
  - (* le_S *) (* Stucks! *) Abort.

But as I mentioned above it is impossible to go further. Another way is to use inversion which is smarter but in some cases it may not help since induction hypothesis would be necessary. But it worth to know about it.

Theorem Sn_le_Sm__n_le_m : forall n m,
  S n <= S m -> n <= m.
Proof.
  intros n m HS.
  inversion HS.
  - (* le_n *) apply le_n.
  - (* le_S *) (* Stucks! *) Abort.

Best way to solve the problem is use of remember tactic as follows.

Theorem Sn_le_Sm__n_le_m : forall n m,
  S n <= S m -> n <= m.
Proof.
  intros n m HS.
  remember (S n) as Sn.
  remember (S m) as Sm.
  induction HS as [ n' | n' m' H IH].
  - (* le_n *)
    rewrite HeqSn in HeqSm. injection HeqSm as Heq.
    rewrite <- Heq. apply le_n.
  - (* le_S *) (* Stucks! *) Abort.

According to Software Foundations (Vol 1: Logical Foundations)

The tactic remember e as x causes Coq to (1) replace all occurrences of the expression e by the variable x, and (2) add an equation x = e to the context.

Anyway, although it is impossible to prove the fact using induction on HS -imo-, performing an induction on m will solve the case. (Note the use of inversion.)

Theorem Sn_le_Sm__n_le_m : forall n m,
  S n <= S m -> n <= m.
Proof.
  intros n.
  induction m as [|m' IHm'].
  - intros H. inversion H as [Hn | n' contra Hn'].
    + apply le_n.
    + inversion contra.
  - intros H. inversion H as [HnSm' | n' HSnSm' Heq].
    + apply le_n.
    + apply le_S. apply IHm'. apply HSnSm'.
Qed.
like image 184
Kamyar Mirzavaziri Avatar answered Oct 23 '22 19:10

Kamyar Mirzavaziri


Just more examples of Kamyar's answer. Well, let's take a look of le induction scheme :

Compute le_ind.

forall (n : nat) (P : nat -> Prop),
       P n ->
       (forall m : nat, n <= m -> P m -> P (S m)) ->
       forall n0 : nat, n <= n0 -> P n0

P is some proposition that holds one natural number, which means in the case of le_n, our preposition n <= m will be reduced to forall n, n <= m. Indeed, it's the same lemma that we want to prove, however unprovable because there is no premise.

An easy to solve this is doing induction where le_ind doesn't do.

For example :

Theorem Sn_le_Sm__n_le_m' : forall m n,
  S n <= S m -> n <= m.
 elim.
 by intros; apply : Gt.gt_S_le .
 intros; inversion H0.
 by subst.
 by subst; apply : le_Sn_le.
Qed.

Notice that we doing induction by m, and using inversion to generates the two possible construction of le ({x = y} + {x < y}). Optionally, you can use le decidability.

Theorem Sn_le_Sm__n_le_m : forall n m,
  S n <= S m -> n <= m.
  intros.
  generalize dependent n.
  elim.
  auto with arith.
  intros.
    have : n <= m.
    by apply : H; apply : le_Sn_le.
  move => H'.
  destruct m.
  auto with arith.
  destruct (le_lt_eq_dec _ _ H').
  assumption.
  subst.
  (* just prove that there is no S m <= m *) 
Qed.

For the sake of your time, coq has the tactic dependent induction that easily solves your goal :

Theorem Sn_le_Sm__n_le_m'' : forall n m,
  S n <= S m -> n <= m.
 intros.
 dependent induction H.
 auto.
 by apply : (le_Sn_le _ _ H).
Qed.
like image 27
Tiago Campos Avatar answered Oct 23 '22 19:10

Tiago Campos