Последствия как функции в Coq?

Question

Я читал, что последствия являются функциями. Но мне трудно понять пример, приведенный на вышеупомянутой странице:

Термин доказательства для импликации P → Q - это функция, которая принимает доказательства для P в качестве входных данных и выдает доказательства для Q в качестве своих выходных данных.

Лемма silly_implication: (1 + 1) = 2 → 0 × 3 = 0. Доказательство. Вступление Н. Рефлексивность. QED.

Мы можем видеть, что доказательный член для вышеприведенной леммы действительно является функцией:

Распечатать silly_implication. (* ===> silly_implication = fun _: 1 + 1 = 2 => eq_refl: 1 + 1 = 2 -> 0 * 3 = 0 *)

Действительно, это функция. Но его тип не выглядит правильным для меня. Из моего прочтения, термин для доказательства P -> Q должна быть функция с доказательством Q в качестве вывода. Затем вывод (1+1) = 2 -> 0*3 = 0 должно быть доказательством 0*3 = 0, один, верно?

Но распечатка Coq выше показывает, что функция изображения eq_refl : 1 + 1 = 2 -> 0 * 3 = 0, вместо eq_refl: 0 * 3 = 0, Я не понимаю, почему гипотеза 1 + 1 = 2 должен появиться в выводе. Может кто-нибудь помочь объяснить, что здесь происходит?

Благодарю.

Answer 1

Ваше понимание верно, пока:

Но распечатка Coq выше показывает, что функция image...

Я думаю, что вы неправильно поняли Print команда. Print показывает вам термин, связанный с определением, а также тип определения. Он не показывает изображение / вывод функции.

Например, следующий выводит определение и тип значения x:

Definition x := 5.
Print x.
> x = 5 
>   : nat

Точно так же следующее печатает определение и тип функции f:

Definition f := fun n => n + 2.
Print f.
> f = fun n : nat => n + 2
>   : nat -> nat

Если вы хотите увидеть кодовый домен функции, вы должны применить функцию к значению, например так:

Definition fx := f x.
Print fx.
> fx = f x
>    : nat

Если вы хотите увидеть изображение / вывод функции Print не поможет тебе Что вам нужно Compute, Compute берет термин (например, приложение функции) и сокращает его, насколько это возможно:

Compute (f x).
> = 7
> : nat