Доказательство теорем об индуктивных типах с помощью _ind; Правило приложения - PullRequest
Новая
       7

Доказательство теорем об индуктивных типах с помощью _ind; Правило приложения

0 голосов
/ 15 сентября 2018 
Variables A B : Prop.

Theorem proj1 : A /\ B -> A.

Чтобы научиться, я пытаюсь доказать эту теорему, явно записав проверочный член с использованием and_ind.

Я бы предположил, что правильный термин для доказательства равен 

fun (H : A /\ B) => and_ind A B A (fun a _ => a) H

Но возникает ошибка, и вместо этого правильный термин равен 

fun (H : A /\ B) => and_ind (fun a _ => a) H

Я не знаюЯ не понимаю этого.Определение and_ind: 

and_ind = 
fun (A B P : Prop) (f : A -> B -> P) (a : A /\ B) => match a with
                                                     | conj x x0 => f x x0
                                                     end
     : forall A B P : Prop, (A -> B -> P) -> A /\ B -> P

Как из этого видно, что параметры (A B P : Prop) должны быть пропущены?

Правило "приложения"

App rule

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

1 Ответ

0 голосов
/ 15 сентября 2018

В Coq вы можете объявить некоторые аргументы функции как неявные .Когда вы вызываете функцию, вы не предоставляете значения для неявных аргументов;Coq автоматически пытается определить подходящие значения, основываясь на другой информации, доступной во время проверки типа.Аргументы A, B и P and_ind все объявлены как неявные и могут быть выведены из типа аргумента H и типа результата аргумента функции.

Вы можете увидеть, какие аргументы считаются неявными, с помощью команды About: 

About and_ind.
(* and_ind : forall A B P : Prop, (A -> B -> P) -> A /\ B -> P *)

(* Arguments A, B, P are implicit *)
(* Argument scopes are [type_scope type_scope type_scope function_scope _] *)
(* and_ind is transparent *)
(* Expands to: Constant Coq.Init.Logic.and_ind *)

Вы можете отключить неявные аргументы с помощью отдельного вызова со знаком @: 

Check fun A B H => @and_ind A B A (fun a _ => a) H.
(* fun (A B : Prop) (H : A /\ B) => and_ind (fun (a : A) (_ : B) => a) H *)
(*      : forall A B : Prop, A /\ B -> A *)

(Обратите внимание, что Coq автоматически пропускает неявные аргументы и при печати термина.)

В руководстве Coq содержится дополнительная информация по этому вопросу.

...