Что такое подцель "нац" - PullRequest
Новая
       10

Что такое подцель "нац"

2 голосов
/ 12 мая 2019

Пытаясь доказать лемму, я попадаю в ситуацию, когда остается только одна подцель, а именно: nat: 

1 subgoal
...
______________________________________(1/1)
nat

Я не совсем понимаю, что это значит.Что мне на самом деле нужно доказать?Имеется ли какая-либо документация по этому вопросу (коуч-вопросы невероятно трудно найти в Google)?

Я не хочу делиться фактической леммой, потому что это задание.По сути, я пытаюсь доказать индуктивное определение, которое выглядит примерно так: 

Inductive indef : deftype -> Prop :=
| foo x : indef (construct_0 x)
| bar a : (forall x, some_predicate x a) -> indef (construct_1 a).

В доказательстве я могу показать, что (forall x : nat, some_predicate x a).Хотя предикат some_predicate определен только для nat, я подозреваю, что проблема связана с тем, что тип x явно не указан в определении indef.Может ли это быть причиной того, что я вижу подцель nat?

Ответы [ 2 ]

1 голос
/ 14 мая 2019

Вот пример, но я не думаю, что он подходит для вашего случая использования. У меня есть функция, которая производит доказательство логического утверждения, но эта функция требует целое число. Это целое число на самом деле бесполезно для доказательства, но для ввода причины любое использование этой функции потребует этого целого числа. 

Definition my_fun (n : nat) : True := I.

Lemma dummy_setup : True.
Proof. apply my_fun.

Итак, на данный момент функции my_fun требуется аргумент типа nat, который больше нигде не используется, но должен существовать. Система Coq обрабатывает этот аргумент так, как если бы он был доказательством, необходимым для логических целей, поэтому он требует, чтобы вы предоставили элемент этого типа. Часто это показывает, что вы спроектировали свои функции плохим образом и что они принимают аргументы, которые они не используют. Чтобы избежать этого, вернитесь к своим леммам и убедитесь, что у них нет бесполезных аргументов.

Вот еще один пример. Лемма my_trans принимает бесполезный аргумент. 

Require Import Arith.
Lemma my_trans : forall x y z t, x <= y -> y <= z -> x <= z.
Proof.  intros x y z; apply (le_trans x y z). Qed.

При использовании этой леммы появляется необходимость в дополнительном аргументе. Механизм доказательства только ожидает, что я покажу, что существует какое-то натуральное число, чтобы заполнить это место. 

Lemma toto x y z : y <= z -> x <= y -> x <= z.
intros h1 h2; revert h2 h1; apply my_trans.

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

0 голосов
/ 15 мая 2019

Пока тип результата вашей леммы равен Prop, Coq на самом деле не волнует, как вы заполняете подцели во время его доказательства. Заполняя подцели, вы, по сути, предоставляете значение этого типа цели.

Примите во внимание следующее:

Если вы встретите цель True, вы можете явно заполнитьцель путем предоставления значения типа True, а именно I.На языке тактики вы могли бы написать: 

1 subgoal
______________________________________(1/1)
True

exact I.     (* explicit way, or  *)
constructor. (* less explicit way *)

No more subgoals.

Иметь цель типа nat - это то же самое.Очевидно, что O является значением типа nat (как и любое натуральное число, например 12432523547835), поэтому вы можете заполнить его следующим образом: 

1 subgoal
______________________________________(1/1)
nat

exact O.              (* this obviously works *)
exact 12432523547835. (* this does work too   *)

No more subgoals.

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

Definition double (x : nat) : nat := x + x.

может быть определена таким образом (однако не делайте этого, если целевой тип не является сложным зависимым типом и результат не может быть легко сформулирован классическим способом): 

Definition double (x : nat) : nat.

1 subgoal
x : nat
______________________________________(1/1)
nat

exact (x + x).  (* Fill the goal with desired value *)

No more subgoals.

Defined.      (* Use this instead of Qed to allow Coq to unfold the definition *)
Print double. (* Checking that the function body is correct *)

double = fun x : nat => x + x
     : nat -> nat

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

...