Используйте теоремы эквивалентности в предложениях больше, чем в Coq - PullRequest
Новая
       5

Используйте теоремы эквивалентности в предложениях больше, чем в Coq

0 голосов
/ 10 апреля 2020

У меня есть следующие определения операций для Эквивалентность, Меньше, чем и сложение в контексте натуральных чисел: 

Require Import Setoid.

(* CNat Set *)
Parameter (CNat:Set) (O i:CNat).

(* CEq Equivalence *)
Parameter CEq: CNat->CNat->Prop.
Infix "¦" := CEq (at level 70, no associativity).
Axiom ceq_refl: forall x:CNat, x¦x.
Axiom ceq_sym: forall x y:CNat, x¦y->y¦x.
Axiom ceq_trans: forall x y z:CNat, x¦y->y¦z->x¦z.
Add Relation CNat CEq
  reflexivity proved by ceq_refl
  symmetry proved by ceq_sym
  transitivity proved by ceq_trans
  as ceq_rel.

(* CLe StrictOrder *)
Parameter CLe: CNat->CNat->Prop.
Infix "«" := CLe (at level 70).
Axiom cle_irrefl: forall x:CNat, ~x«x.
Axiom cle_trans: forall x y z:CNat, x«y->y«z->x«z.
Add Relation CNat CLe
  transitivity proved by cle_trans
  as cle_rel.

(* CAdd Operation *)
Parameter CAdd : CNat->CNat->CNat.
Infix "±" := CAdd (at level 50, left associativity).
Add Morphism CAdd with signature CEq ==> CEq ==> CEq 
  as ceq_add_mor. Admitted.

Затем я определяю нейтральное сложение и естественную индукцию и пытаюсь использовать их внутри теоремы теста: 

(* CNat Axioms *)
Axiom cnat_add_neutral: forall x:CNat, x±O¦x.
Axiom cnat_induction: forall P: CNat->Prop, P O ->
    (forall x:CNat, P x->P (x±i)) -> forall x:CNat, P x.

(* CNat Test Theorem *)
Example cle_neutral_test: forall x:CNat, O«x -> O«x±O.
Proof.
  intros x CH.
  rewrite cant_add_neutral. (* Error *)
  apply CH.
Qed.

Со следующей ошибкой: 

Error:
Tactic failure: setoid rewrite failed: Unable to satisfy the following constraints:
In environment:
x : CNat
CH : O « x
do_subrelation := Morphisms.do_subrelation : Morphisms.apply_subrelation

?p : "Morphisms.Proper (CEq ==> Basics.flip Basics.impl) (CLe O)"

Какой вид предыдущего определения или демонстрации я должен сгенерировать, прежде чем смогу сделать этот Тест работоспособным?

1 Ответ

1 голос
/ 11 апреля 2020

(используя более стандартную запись, я надеюсь, что вам все еще ясно. CEq - это ==, CLe - это < (его, вероятно, следует назвать CLt))

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

Вы хотите доказать x < y, и вы знаете y == z. Для этого вы хотели бы, чтобы следующая лемма изменила цель на x < z: 

y == z -> x < z -> x < y

Это в настоящее время отсутствует в списке фактов.

Один способ представить этот факт соответствующим образом для обобщенного переписывания - это Morphism объявление для CLe: 

Add Morphism CLe with signature CEq ==> CEq ==> iff
  as ceq_cle_mor. Admitted.

Подпись CEq ==> CEq ==> iff означает: 

forall x x',
  x == x' ->
  forall y y',
  y == y' ->
  (x < y) <-> (x' < y')

То, что можно легко проверить, является обобщением пропущенный факт выше. Добавив его и исправив опечатку в лемме cnat_add_neutral (в первоначальной версии вашего вопроса, теперь отредактированной), доказательство проходит. 

Add Morphism CLe with signature CEq ==> CEq ==> iff
  as ceq_cle_mor. Admitted.

(* CNat Test Theorem *)
Example cle_neutral_test: forall x:CNat, O«x -> O«x±O.
Proof.
  intros x CH.
  rewrite cnat_add_neutral.
  apply CH.
Qed.
...