Как переписать «+ 1» (плюс один) в «S» (succ) в Coq?

Question

У меня есть следующая лемма с неполным доказательства:

Lemma (s_is_plus_one : forall n:nat, S n = n + 1). 
Proof. 
    intros. 
    reflexivity. 
Qed. 

Это доказательство терпит неудачу с

Unable to unify "n + 1" with "S n". 

Похоже eq_S бы способ доказать это, но я не могу применить его (он не признает n + 1 как S n: Error: Unable to find an instance for the variable y.). Я также пробовал ring, но он не может найти отношения. Когда я использую rewrite, он просто сводится к той же конечной цели.

Как я могу закончить это доказательство?

Answer 1

Это связано с тем, как определяется (+). Вы можете получить доступ к (+) «s основного определения пути включения нотации выключение (в CoqIDE, которая находится в View > Display notations), видя, что обозначение (+) соответствует функции Nat.add и затем вызвать Print Nat.add, который дает вам:

Nat.add = 
fix add (n m : nat) {struct n} : nat := 
    match n with 
    | O => m 
    | S p => S (add p m) 
    end 

Вы можете увидеть, что (+) определяется путем сопоставления по первому аргументу, который в n + 1 является переменной n. Потому что n не начинается ни с O, ни с S (это не «конструктор-голова»), match не может уменьшить. Это означает, что вы не сможете доказать равенство, просто сказав, что две вещи вычисляются в одну и ту же нормальную форму (что и утверждает reflexivity).

Вместо этого вам нужно объяснить coq, почему это так, что для любого n будет выполнено равенство. Классический ход в случае рекурсивной функции, такой как Nat.add, состоит в том, чтобы приступить к доказательству induction. И это действительно сделать работу здесь:

Lemma s_is_plus_one : forall n:nat, S n = n + 1. 
Proof. 
intros. induction n. 
- reflexivity. 
- simpl. rewrite <- IHn. reflexivity. 
Qed. 

Другая вещь, которую вы можете сделать, это уведомление, что 1 с другой стороны, конструктор возглавляемые, который означает, что матч будет стрелять, если только у вас 1 + n, а не n + 1. Ну, мы в удаче, потому что в стандартной библиотеке кто-то уже доказано, что Nat.add коммутативен поэтому мы можем использовать только что:

Lemma s_is_plus_one : forall n:nat, S n = n + 1. 
Proof. 
intros. 
rewrite (Nat.add_comm n 1). 
reflexivity. 
Qed. 

последней альтернативы: с помощью SearchAbout (?n + 1), мы можем найти все теоремы говорить о шаблон ?n + 1 для некоторых переменных ?n (знак вопроса важен здесь). Первый результат - действительно релевантная лемма:

Nat.add_1_r: forall n : nat, n + 1 = S n