применять тактику работает, но переменные цели и гипотезы разные - PullRequest
Новая
       24

применять тактику работает, но переменные цели и гипотезы разные

0 голосов
/ 10 июня 2019

Играя с теоремой leb_complete из IndProp, я обнаружил следующую странность: 

Theorem leb_complete : forall n m,
  n <=? m = true -> n <= m.
Proof.
  induction n as [|n'].
  - intros. apply O_le_n.
  - induction m as [| m'] eqn:Em.
    + intros H. discriminate H.
    + intros H. apply n_le_m__Sn_le_Sm.

Производит следующее: 

1 subgoal (ID 155)

n' : nat
IHn' : forall m : nat, (n' <=? m) = true -> n' <= m
m, m' : nat
Em : m = S m'
IHm' : m = m' -> (S n' <=? m') = true -> S n' <= m'
H : (S n' <=? S m') = true
============================
n' <= m'

Все хорошо. Теперь, когда я запускаю apply IHn'., он работает и выдает следующее: 

(n' <=? m') = true

Почему это работает? В IHn 'у нас есть 

n' <= m - in IHn'
n' <= m' - in the goal

Переменные m и m' различны, но все равно работает. Когда я пытался 

`rewrite -> Em in IHn'.

выдал ошибку: 

Found no subterm matching "m" in IHn'.

Но в IHn 'есть переменная "m"! Я запутался, пожалуйста, объясните, что здесь происходит.

1 Ответ

4 голосов
/ 10 июня 2019

m в IHn' - просто фиктивная переменная. IHn' количественно определяет все натуральные числа: forall m : nat, [...]. В частности, m' - это nat, поэтому гипотеза применима с заменой m на m'.

m в IHn' - это не то же самое, что в вашем контексте (и, в частности, не то же самое, что m в Em : m = S m'). У них просто одно и то же имя.

...