Интерпретировать термин как тип в Coq

Question

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

The term "x = x" has type "Prop" while it is expected to have type "x = x".

, которая также генерируется следующим MRE:

Require Import Setoid.

(* Custom natural Set *)
Parameter CNat : Set.

(* Addition *) 
Parameter CAdd : CNat -> CNat -> CNat. 
Infix "±" := CAdd (at level 50, left associativity).

(* Addition Morphism *)
Axiom cnat_add_morphism : 
  forall (x x' : CNat), x = x' ->
  forall (y y' : CNat), y = y' -> 
    x ± y = x' ± y'.

(* Test Example *)
Example cnat_add_inc : 
  forall (x y c : CNat), x = y -> x±c = y±c.
Proof.
  intros x y c CH.
  rewrite (@cnat_add_morphism x x (x=x) c c (c=c)). (* #Error *)

Можно ли сказать cnat_add_morphism (что в моем коде является теоремой вместо аксиомы) интерпретировать термины x¦x и c¦c как тип, чтобы заставить морфизм работать должным образом, или другой, чтобы можно было применить ручное переписывание морфизма вместо добавления его как сетоид?

Answer 1

Здесь есть несколько проблем.

Прежде всего , ошибка означает, что вы пытаетесь дать cnat_add_morphism предложение вместо доказательства этого предложения. В Coq доказательства являются объектами типа предложения, доказательством которого они являются. например, forall x : CNat, x¦x является типом, и вы должны создать объект этого типа, чтобы гарантировать, что тип является истинным. Это похоже на то, что у вас есть функция f : nat -> nat и вы пишете f nat, вы получаете следующую ошибку:

The term "nat" has type "Set" while it is expected to have type "nat".

Полученная вами ошибка точно такая же. Таким образом, вам нужно предоставить объект типа "x" x ", т. Е. Доказательство, которое гарантирует, что предложение x ¦ x верно. Таким образом, вы можете использовать аксиому ceq_reflexivity. Термин (ceq_reflexivity x) имеет тип x¦x, и вы можете использовать его вместо неправильного использования x¦x.

(cnat_add_morphism x x (ceq_reflexivity x))

Second , вам нужно применить лемму, а не переписывать и используйте предположение вместо x¦x (используйте x и y не только x).

apply (cnat_add_morphism x y CH c c (ceq_reflexivity c)).

Answer 2

Первая проблема, с которой вы столкнулись, заключается в том, что термин, который вы хотите переписать, напечатан неправильно:

cnat_add_morphism x x (x¦x) c c (c¦c)

У вас есть

cnat_add_morphism x x : x¦x -> forall y y', y¦y' -> x ± y ¦ x ± y'

, поэтому вам необходимо предоставить подтверждение x¦x но вы предоставляете x¦x сам. Вам на самом деле нужно добавить доказательства рефлексивности в вашей системе. Что-то вроде

Parameter CRefl : forall (x : CNat), x¦x.

Тогда вы можете доказать свою лемму.

Example cnat_add_inc : 
  forall (x y c : CNat), 
    x¦y -> 
    x ± c ¦ y ± c.
Proof.
  intros x y c CH.
  apply cnat_add_morphism.
  - assumption.
  - apply CRefl.
Qed.