Как доказать определение доказательства в Coq

В настоящее время я работаю с Coq, и у меня возникла проблема, которую я не знаю, как решить.

Допустим, мы работаем с заданным типом, я возьму nat в качестве примера и хочу использовать функцию f, которая может дать сбой. Чтобы компенсировать сбой, мы определяем f как тип nat -> option nat.

Теперь у меня есть заданная гипотеза H: nat -> bool, при которой f не ошибается, и я даже доказал лемму

Lemma no_error_in_f : forall (n:nat), H n = true -> exists (u:nat), f n = Some u.

Я хочу определить функцию g: nat->nat, которая дает результат f на n, если H n удовлетворен, и просто дает n в противном случае. Эта функция должна быть четко определена, но я не знаю, как ее правильно определить. Если я попробую что-то наивное, например Definition g (n:nat) := if H n then f n else n., проблема в системе набора текста.

Кто-нибудь знает, как собрать все элементы и сообщить системе, что определение допустимо?


types pattern-matching definition coq proof
person tben    schedule 23.01.2016    source источник

Ответы (3)


arrow_upward
1
arrow_downward

Я даю здесь решение, которое работает с теми же гипотезами, что и выдвинутые в вопросе.

Axiom f : nat -> option nat.
Axiom H : nat -> bool.
Axiom no_error_in_f : forall n,
  H n = true -> exists u, f n = Some u.

Lemma no_error_in_f_bis : forall n,
  H n = true -> f n <> None.
Proof.
  intros. apply no_error_in_f in H0. destruct H0. rewrite H0. discriminate.
Qed.

Definition g n :=
  match H n as b return H n = b -> _ with
  | true => fun H =>
    match f n as f0 return f n = f0 -> _ with
    | Some n0 => fun _ => n0
    | None => fun H0 => match no_error_in_f_bis n H H0 with end
    end eq_refl
  | false => fun _ => n
  end eq_refl.

Я использую другую лемму, чем no_error_in_f, что удобнее доказывать False. Обратите внимание, что две идеи этой функции (использовать конструкцию return для match, уничтожить доказательство False, чтобы показать, что ветвь недоступна) объясняются здесь: http://adam.chlipala.net/cpdt/html/Subset.html.

person eponier    schedule 24.01.2016

arrow_upward
0
arrow_downward

В вашем развитии есть две проблемы. Во-первых, вы не можете использовать no_error_in_f для определения g в Coq без допущения дополнительных аксиом, потому что Coq не позволяет извлекать вычислительную информацию из доказательства (проверьте здесь, чтобы получить более подробную информацию). Другая проблема заключается в том, что вы не можете использовать H в выражении if, потому что оно возвращает Prop вместо bool (проверьте этот ответ для получения дополнительных сведений).

person Arthur Azevedo De Amorim    schedule 23.01.2016
comment
Извините, я допустил ошибку, вторая ошибка не появляется, потому что H n имеет тип bool, а моя лемма имеет предикат H n = true. Я это отредактирую. Для первой проблемы я придумал что-то вроде False_rec или что-то в этом роде - person tben; 24.01.2016

arrow_upward
0
arrow_downward

Я нашел способ сделать это, вот мое решение, если кому-то интересно:

Definition g (n:nat) :nat := (match (H n) as a return a = H n -> nat with | true => (fun H_true => (match (f n) as b return b = f n -> nat with | Some u => (fun _ => u) | None => (fun H1 => False_rec _ (no_error_in_f H_true H1)) end) (eq_refl f n)) | false => n end) (eq_refl H n).

Для тех, кто хотел бы знать, что это означает, False_rec принимает в качестве второго аргумента доказательство False и удостоверяет, что сопоставление невозможно. срок

(match (f n) as b return b = f n -> nat with | Some u => (fun _ => u) | None => (fun H1 => False_rec _ (no_error_in_f H_true H1)) end) (eq_refl f n)) имеет тип f n = f n-> nat, и когда я применяю его к доказательству eq_refl (f n) (которое является доказательством того, что f n = f n, так набрано f n = f n), я получаю nat. Этот трюк позволяет мне получить H1, которое является доказательством, которое f n = None получено с использованием рефлексивности равенства и сопоставления с образцом, и которое я собираюсь использовать в своем доказательстве False.

То же самое и с другим матчем.

person tben    schedule 24.01.2016
comment
Я понимаю идею, но ваше решение не проверяется типом как есть. Не могли бы вы исправить это, чтобы он работал с гипотезами, приведенными в вашем вопросе? - person eponier; 24.01.2016