Индукция на доказательство для отношения «меньше, чем» в coq - PullRequest
Новая
       97

Индукция на доказательство для отношения «меньше, чем» в coq

0 голосов
/ 24 мая 2019

Я работаю над доказательством следующей теоремы Sn_le_Sm__n_le_m в IndProp.v из Основы программного обеспечения (Том 1: Логические основания) . 

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.

где, определение le (i.e., ≤): 

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).

До induction HS контекст и цель заключаются в следующем: 

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

В пункте первой маркированной строки - контекст и цель: 

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

где мы должны доказать n <= m без какого-либо контекста, что, очевидно, невозможно.

Почему он не генерирует S n = S m (а затем n = m) для случая le_n в induction HS?

...