Блог

Я пытаюсь доказать групповые аксиомы для типа Z_3:

 Require Import Coq.Arith.PeanoNat.

Record Z_3 : Type := Z3
{
  n :> nat;
  proof : (Nat.ltb n 3) = true
}.

Proposition lt_0_3 : (0 <? 3) = true.
Proof.
  simpl. reflexivity.
Qed.

Definition z3_0 : Z_3 := (Z3 0 lt_0_3).

Proposition lt_1_3 : (1 <? 3) = true.
Proof.
  reflexivity.
Qed.

Definition z3_1 : Z_3 := (Z3 1 lt_1_3).

Proposition lt_2_3 : (2 <? 3) = true.
Proof.
  reflexivity.
Qed.

Definition z3_2 : Z_3 := (Z3 2 lt_2_3).

Proposition three_ne_0 : 3 <> 0.
Proof.
  discriminate.
Qed.

Lemma mod_upper_bound_bool : forall (a b : nat), (not (eq b O)) -> (Nat.ltb (a mod b) b) = true.
Proof.
  intros a b H. apply (Nat.mod_upper_bound a b) in H. case Nat.ltb_spec0.
  - reflexivity.
  - intros Hcontr. contradiction.
Qed.

Definition Z3_op (x y: Z_3) : Z_3 :=
  let a := (x   y) mod 3 in
  Z3 a (mod_upper_bound_bool _ 3 three_ne_0).

Lemma Z3_eq n m p q : n = m -> Z3 n p = Z3 m q.
Proof.
  intros H. revert p q. rewrite H. clear H. intros. apply f_equal.
  

Мы почти закончили:

 1 subgoal (ID 41)
  
  n, m : nat
  p, q : (m <? 3) = true
  ============================
  p = q
  

Какую теорему я должен использовать, чтобы доказать, что p = q?

Обновление 1

 Theorem bool_dec :
  (forall x y: bool, {x = y}   {x <> y}).
Proof.
  intros x y. destruct x.
  - destruct y.
      left. reflexivity.
      right. intro. discriminate H.
  - destruct y.
      right. intro. discriminate H.
      left. reflexivity.
Qed.

Lemma Z3_eq n m p q : n = m -> Z3 n p = Z3 m q.
Proof.
  intros H. revert p q. rewrite H. clear H. intros. apply f_equal. apply UIP_dec. apply bool_dec.
Qed.
  

Вам, вероятно, интересно знать, что каждые два доказательства разрешимого равенства равны. Это объясняется и доказывается здесь: https://coq.inria.fr/library/Coq.Logic.Eqdep_dec.html

Вас интересует, в частности, лемма UIP_dec : https://coq.inria.fr/library/Coq.Logic.Eqdep_dec.html#UIP_dec

 Theorem UIP_dec :
  forall (A:Type),
    (forall x y:A, {x = y}   {x <> y}) ->
    forall (x y:A) (p1 p2:x = y), p1 = p2.
  

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

Это другой вопрос, но поскольку вы спросили: bool_dec существует и даже имеет это имя! Простой способ найти это — использовать команду

 Search sumbool bool.
  

Это приведет к появлению нескольких лемм, в том числе довольно ранних:

 Bool.bool_dec: forall b1 b2 : bool, {b1 = b2}   {b1 <> b2}
  

Почему я искал sumbool ? sumbool это тип, который написан выше:

 { A }   { B } := sumbool A B
  

Вы можете найти его с помощью очень хорошей Locate команды:

 Locate "{".
  

появится

 "{ A }   { B }" := sumbool A B : type_scope (default interpretation)
  

(и другие обозначения, включающие «{«).