Coq: Доказательство применения

Question

Это немного теоретический вопрос. Мы можем определить fx, но казалось бы, не fx':

Function fx {A} (x:A) (f:A->Type) (g:Type->f x): f x := g (f x). 
Definition fx' {A} (x:A) (f:A->Type): f x. 

В некотором смысле, это имеет смысл, так как никто не может доказать, из f и x что f уже был (или будет) применяться к x. Но мы можем применить f к x, чтобы получить что-то типа Type:

assert (h := f x). 

Это кажется странным: можно применить к fx но еще не может получить свидетельство y: f x, что он сделал это.

Единственное объяснение, которое я могу придумать, это следующее: как тип, f x - это приложение, как термин, это всего лишь тип. Мы не можем вывести прошлую заявку из типа; аналогично, мы не можем вывести будущее приложение из функции и ее потенциального аргумента. Что касается (экземпляра) применения себя, это не этап доказательства, поэтому мы не можем быть свидетелем этого. Но я просто догадываюсь. Вопрос:

Можно ли определить fx'? Если да, то как; если нет, то почему (просьба дать теоретическое объяснение)

Answer 1

Во-первых, прямой ответ на ваш вопрос: не, не представляется возможным определить fx'. По вашему сниппета, fx' должен иметь тип

forall (A : Type) (x : A) (f : A -> Type), f x. 

Это не трудно понять, что существование fx' влечет противоречие, так как следующий сценарий показывает.

Section Contra. 

Variable fx' : forall (A : Type) (x : A) (f : A -> Type), f x. 

Lemma contra : False. 
Proof. 
    exact (fx' unit tt (fun x => False)). 
Qed. 

End Contra. 

Что здесь произошло? Тип fx' говорит, что для любого семейства типов f, индексированного по типу A, мы можем изготовить элемент f x, где x является произвольным. В частности, мы можем принять f как постоянное семейство типов (fun x => False), и в этом случае f x - это то же самое, что и False. (Обратите внимание, что False, помимо того, что является членом Prop, также является членом Type.)

Теперь, учитывая ваш вопрос, я думаю, что вы немного смущен по смыслу типов и предложений в Coq. Вы сказали:

Это кажется загадочным: можно применить к fx, но до сих пор не может получить свидетельство y: f x, что он сделал это.

Тот факт, что мы можем применить f к x просто означает, что выражение f x имеет действительный тип, который, в данном случае, является Type. Другими словами, Coq показывает, что f x : Type.Но, имея тип, это другое дело: проживает: когда f и x произвольны, невозможно построить термин y такой, что y : f x. В частности, у нас есть False : Type, но мы не можем построить термин p с p : False, потому что это будет означать, что логика Кока непоследовательна.