Как я могу сделать пример для сигма-типа в Coq? - PullRequest
Новая
       18

Как я могу сделать пример для сигма-типа в Coq?

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

Для этого типа: 

Record Version := mkVersion { 
  major  : nat; 
  minor  : nat; 
  branch : {b:nat| b > 0 /\ b <= 9};
  hotfix : {h:nat| h > 0 /\ h < 8} 
}.

Я пытаюсь сделать пример: 

Example ex1 := mkVersion 3 2 (exist _ 5) (exist _ 5).

И это не удалось с:

Термин«Существует? P 5» имеет тип «? P 5 -> {x: nat |? P x}», в то время как ожидается, что он будет иметь тип «{b: nat | b> 0 / \ b <= 9}». </p>

Чего мне не хватает?

1 Ответ

5 голосов
/ 29 мая 2019

Причина, по которой он не работает, заключается в том, что вам нужно не только предоставить свидетеля (b и h в данном случае), но и доказательство того, что соответствующее условие выполняется для предоставленного свидетеля.

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

From Coq Require Import Bool Arith.

Coercion is_true : bool >-> Sortclass.

Record Version := mkVersion {
  major  : nat;
  minor  : nat;
  branch : {b:nat| (0 <? b) && (b <=? 9)};
  hotfix : {h:nat| (0 <? h) && (h <? 8)}
}.

Example ex1 := mkVersion 3 2 (exist _ 5 eq_refl) (exist _ 5 eq_refl).

Мы могли бы ввести нотацию, обеспечивающую более хорошее представление литералов:

Notation "<| M ',' m ',' b '~' h |>" :=
  (mkVersion M m (exist _ b eq_refl) (exist _ h eq_refl)).

Example ex2 := <| 3,2,5~5 |>.

Если необходимо добавить ручные доказательства, я бы предложил использовать механизм Program: 

From Coq Require Import Program.

Program Definition ex3 b h (condb : b =? 5) (condh : h =? 1) :=
  mkVersion 3 2 (exist _ b _) (exist _ h _).
Next Obligation.
  now unfold is_true in * |-; rewrite Nat.eqb_eq in * |-; subst. Qed.
Next Obligation.
  now unfold is_true in * |-; rewrite Nat.eqb_eq in * |-; subst. Qed.

или refine тактика: 

Definition ex3' b h (condb : b =? 5) (condh : h =? 1) : Version.
Proof.
  now refine (mkVersion 3 2 (exist _ b _) (exist _ h _));
  unfold is_true in * |-; rewrite Nat.eqb_eq in * |-; subst.
Qed.
...