Можно ли доказать теоремы в coq (или вообще) без использования ранее доказанных лемм?

Question

Учитывая, что доказательства в coq - это просто очень сложные функции, которые могут быть построены любым из множества способов, кажется, имеет смысл, что будет существовать доказательство coq каждой теоремы, которая не включает в себя ни ранее доказанные теоремы, ни заявления assert.

Например, доказательство коммутативности натуральных тот просто, без чешуй, несмотря на то, что можно было бы сделать проще с чешуями:

Theorem plus_comm' : 
    forall n m : nat, n + m = m + n. 
Proof. 
    induction n. 
    intro m. simpl. induction m. 
     reflexivity. 
     simpl. rewrite <- IHm. reflexivity. 
    intro m. simpl. rewrite -> IHn. induction m. 
     reflexivity. 
     simpl. rewrite <- IHm. reflexivity. 
Qed. 

Но когда я пытаюсь сделать то же самое для коммутативности умножение, я неизбежно сталкиваюсь с ситуацией, когда мне требуется факт о добавлении.

Theorem mult_comm' : 
    forall n m : nat, n * m = m * n. 
Proof. 
    induction n. 
    intro m. simpl. induction m. 
     reflexivity. 
     simpl. apply IHm. 
    intro m. simpl. rewrite -> IHn. induction m. 
     reflexivity. 
     simpl. rewrite <- IHm. f_equal. 
    (* left with goal: 
     m + (n + m * n) = n + (m + m * n) 
    *) 
Abort. 

Почему?

Answer 1

Существует, конечно, доказательство без лемм или утверждений, если есть такое доказательство цели, с которой вы остались, m + (n + m * n) = n + (m + m * n). Вот один, хотя это не очень выяснение:

remember (m*n) as o. 
clear. 
generalize dependent o. 
generalize dependent m. 
induction n; simpl; try reflexivity. 
simpl. 
intros m o. 
rewrite <- (IHn m o). 
remember (n+o) as p. 
clear. 
generalize dependent p. 
induction m; simpl; try reflexivity. 
intros p; rewrite (IHm p). 
reflexivity. 

Вопрос о том, почему вы «необходимость» лемма может рассматриваться с другой точки зрения:

Посмотрите на этом доказательстве коммутативности multiplication.Part из этого является доказательством этого забавного факта о добавлении, что вы можете перемешать круглые скобки вокруг, не изменяя значение. Кажется, это немного похоже на другие доказательства! Возможно, этот факт был бы полезным для упаковки с именем. Затем мы можем ссылаться на него снова и снова, и читатель поймет, о чем мы говорим, и каждый раз ему не понадобится новое доказательство.

Давайте назовем вспомогательный факт «леммой». Мы будем называть процесс его перемещения и давая ему название «рефакторинг».

Answer 2

Логика Кокса имеет значение cut-elimination, что означает, что любое доказательство, связанное с промежуточными леммами (т. Е. Лямбда-терм с бета-редексами), по алгоритму редукции может быть преобразовано в прямое доказательство (т. Е. Член в нормальной форме).

Однако это может произойти за счет экспоненциального раздувания: например, уменьшение power 2 100 (как в функции power, примененной к 2, и 100 произведет термин размер 2^100, начиная с срока 1 + 2 + 100).

Если вы пытаетесь написать алгоритмы поиска доказательств, вы можете захотеть взглянуть на фокусировку. Учитывая, что вы, похоже, хотите сосредоточиться на индуктивных доказательствах, вы можете взглянуть на Boyer & Moore's prover тоже.