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
?
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.
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.
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).
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.
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.
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.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With