Coq Set Наследование

Question

Я доказал много теорем, начиная с действительных аксиом, теперь я хочу определить Naturals как подмножество вещественных чисел и повторно использовать все доказанные теоремы. Как это можно сделать? Вот искусственное MRE, которое компилируется с использованием надлежащих методов проектирования coq:

01  (* CReal Definitions *)
02  Parameter CReal: Set.
03  Parameter creal_add : CReal -> CReal -> CReal.
04  Axiom creal_comm: forall x y:CReal, creal_add x y = creal_add y x.
05   
06  (* CNat Definitions *)
07  Parameter CNat: Set.
08  Theorem cnat_comm: forall x y:CNat, creal_add x y = creal_add y x.
09  Proof. exact creal_comm. Qed. (* Should be OK after subclassing *)

Теперь он жалуется на то, что O является CReal вместо CNat, поэтому было бы здорово, если бы x был полиморфно интерпретирован как CReal, чтобы иметь возможность сравнивать против других CReals и применять к ним теоремы и аксиомы CReal в красивой и не запутанной форме.

EDIT :

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

11  (* CNat Positive *)
12  Parameter O : CReal.
13  Parameter cnat_succ : CNat -> CNat.
14  Axiom cnat_positive: forall (x : CNat), ~cnat_succ x=O.
15
16  (* CReal Wrong Theorem *)
17  Theorem creal_positive: forall x:CReal, ~cnat_succ x=O. (*Crash*)
18  Proof. exact cnat_positive. Qed. (*Also Crash*)

Причина, по которой строки 17 и 18 должны создавать sh, заключается в том, что 17 использует cnat_su cc вместо CReal, но определяется только cnat_su cc для подкласса CNat, а в 18 используется аксиома CNat, которая не должна быть видна суперклассу CReal. Таким образом, аксиомы и теоремы суперкласса должны быть видимы для подкласса и применимы к ним, но не наоборот.

Answer 1

Наконец-то я нашел решение, используя классы типов. Вот расширение Naturals с использованием целых чисел, которое имеет больше смысла, чем расширение Reals с использованием Naturals, они как-то менее специализированы (требуют меньше аксиом), чем первое:

01  (* Import Setoid for smart rewriting *)
02  Require Import Setoid.
03  
04  
05  (* -------------------------------------------------- *)
06  (* CNat Class *)
07  
08  
09  (* CNat Definition *)
10  Class CNat A := {
11    O: A;
12    succ: A->A;
13    add: A->A->A;
14    add_comm: forall x y:A, add x y = add y x
15  }.
16  
17  (* O Commutativity Lemma *)
18  Lemma O_SO `{CNat}: add O (succ O) = add (succ O) O.
19  Proof.
20    apply add_comm.                 (* Class axiom *)
21  Qed.

Это было определение класса CNat и его О_СО Лемма. Теперь определение класса CInt, некоторая нотация и ее лемма invO_O, в которой повторно используются аксиомы суперкласса CNat (аксиома add_comm) и теоремы (лемма O_SO):

24  (* -------------------------------------------------- *)
25  (* CInt Class *)
26  
27  
28  (* CInt Definition *)
29  Class CInt A `{CNat A} := {
30    inv: A->A;
31    add_inv: forall x:A, add x (inv x) = O
32  }.
33  
34  (* Some notation for convenience *)
35  Notation "´ x" := (succ x) (at level 25, right associativity).
36  Infix "±" := add (at level 50, left associativity).
37  Notation "¯ x" := (inv x) (at level 35, right associativity).
38  
39  (* O Additive Inverse Lemma *)
40  Lemma invO_O `{CInt}: (´O±O) ± ¯(O ±´O) = (´O±´´O) ± ¯(´´O ±´O).
41  Proof.
42    rewrite O_SO.                   (* Superclass Lemma *)
43    setoid_rewrite add_comm at 5.   (* Superclass Axiom *)
44    setoid_rewrite add_inv.         (* Class Axiom *)
45    reflexivity.
46  Qed.

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

PD :

Если вы хотите использовать forall x:A вам нужно параметризовать вашу теорему с помощью Generalizable Variables:

48 Generalizable Variables A.
49 (* Commutative Additive Inverse Lemma *)
50 Lemma inv_inv `{CInt A}: forall x:A, ¯x±x=O.
51 Proof.
52   setoid_rewrite add_comm.
53   apply add_inv.
54 Qed.

Answer 2

Вы должны показать, что ваш CNat изоморфен c с подмножеством CReal и что операции CNat закрыты.

Вот пример, который вы можете расширить по своему вкусу. Я доказываю простую лемму, используя lra tacti c, которая используется для реалов.

Я использую принуждения, чтобы мне не пришлось вставлять функции впрыска f и g везде вручную. Они есть, но невидимыми чернилами. Сделайте Set Printing Coercions., если хотите их увидеть.

Require Import Reals.

Open Scope R.
Parameter (N:Type)(f:N->R) (g:R->N).
Parameter iso1: forall x, f (g x) = x.
Parameter iso2: forall x, g (f x) = x.
Coercion f : N>->R.
Coercion g : R>->N.

Parameter (n0 n1 : N) (nplus nmult : N->N->N) .
Parameter nzero : n0 = 0.
Parameter none : n1 = 1.
Parameter nplus_ok : forall a b:N, nplus a b  = a+b.
Parameter nmult_ok : forall a b:N, nmult a b  = a*b.

Set Printing Coercions.
Print nplus_ok.
(*  nplus_ok : forall a b : N, nplus a b = g (f a + f b)  *)
Unset Printing Coercions.

(* useful tactic to rewrite N to R *)
Ltac NtoR :=
  rewrite ?nplus_ok,  ?nmult_ok, ?nzero, ?none,  ?iso1;
  try apply f_equal.

Require Import Psatz.
Goal forall (a b c:N),
    (nplus a (nplus b c)) + nmult 1 (a+n1+c) = nplus (2*nplus c a) (nplus (n0+1) b).
  intros.
  NtoR.
  lra.
Qed.