2
제목에서 알 수 있듯이 제 질문은 Coq에서 산술 표현의 정확성과 전체 평가를 우려합니다. 내가 증명하고자하는 정리는 총 세 가지이다 : 게으른 평가 정확도 및 총계 (Coq)
정리 Only_canonical_results
결과로계산은 정규 식을 제공 : (x 및 y FORALL : Aexp, 경화제의 x 및 y -> 정식 Y).
정확성 : 연산 관계 식의 외연을 보존
정리 된 correct_wrt_semantics : (x 및 y FORALL : Aexp, 경화제의 x 및 y -> I N (외연의 X) (외연의 Y)).
모든 입력은 결과를 가져옵니다.
정리 Comp_is_total : (forall x : Aexp, (Sigma Aexp (fun y => prod (표준형 y))))).
필요한 정의는 아래 첨부 된 코드에서 찾아 볼 수 있습니다. 내가 Coq에 관해서 초보자임을 분명히해야한다. 보다 숙련 된 사용자가 곧바로 알아 차릴 것입니다. 대다수 또는 내가 작성한 배경 자료 모두가 표준 라이브러리에서 발견 될 수있는 경우가 가장 확실합니다. 그러나 원하는 결과를 증명하기 위해 표준 라이브러리에서 가져올 항목을 정확히 알고 있다면, 아마도 여기에 귀찮게하지 않을 것입니다. 그것이 내가 지금까지 가지고있는 자료를 당신에게 제출하는 이유입니다. 어떤 친절한 사람이 나를 도울 수 있기를 바랍니다. 감사!
(* Sigma types *)
Inductive Sigma (A:Set)(B:A -> Set) :Set :=
Spair: forall a:A, forall b : B a,Sigma A B.
Definition E (A:Set)(B:A -> Set)
(C: Sigma A B -> Set)
(c: Sigma A B)
(d: (forall x:A, forall y:B x,
C (Spair A B x y))): C c :=
match c as c0 return (C c0) with
| Spair a b => d a b
end.
Definition project1 (A:Set)(B:A -> Set)(c: Sigma A B):=
E A B (fun z => A) c (fun x y => x).
(* Binary sum type *)
Inductive sum' (A B:Set):Set :=
inl': A -> sum' A B | inr': B -> sum' A B.
Print sum'_rect.
Definition D (A B : Set)(C: sum' A B -> Set)
(c: sum' A B)
(d: (forall x:A, C (inl' A B x)))
(e: (forall y:B, C (inr' A B y))): C c :=
match c as c0 return C c0 with
| inl' x => d x
| inr' y => e y
end.
(* Three useful finite sets *)
Inductive N_0: Set :=.
Definition R_0
(C:N_0 -> Set)
(c: N_0): C c :=
match c as c0 return (C c0) with
end.
Inductive N_1: Set := zero_1:N_1.
Definition R_1
(C:N_1 -> Set)
(c: N_1)
(d_zero: C zero_1): C c :=
match c as c0 return (C c0) with
| zero_1 => d_zero
end.
Inductive N_2: Set := zero_2:N_2 | one_2:N_2.
Definition R_2
(C:N_2 -> Set)
(c: N_2)
(d_zero: C zero_2)
(d_one: C one_2): C c :=
match c as c0 return (C c0) with
| zero_2 => d_zero
| one_2 => d_one
end.
(* Natural numbers *)
Inductive N:Set :=
zero: N | succ : N -> N.
Print N.
Print N_rect.
Definition R
(C:N -> Set)
(d: C zero)
(e: (forall x:N, C x -> C (succ x))):
(forall n:N, C n) :=
fix F (n: N): C n :=
match n as n0 return (C n0) with
| zero => d
| succ n0 => e n0 (F n0)
end.
(* Boolean to truth-value converter *)
Definition Tr (c:N_2) : Set :=
match c as c0 with
| zero_2 => N_0
| one_2 => N_1
end.
(* Identity type *)
Inductive I (A: Set)(x: A) : A -> Set :=
r : I A x x.
Print I_rect.
Theorem J
(A:Set)
(C: (forall x y:A,
forall z: I A x y, Set))
(d: (forall x:A, C x x (r A x)))
(a:A)(b:A)(c:I A a b): C a b c.
induction c.
apply d.
Defined.
(* functions are extensional wrt
identity types *)
Theorem I_I_extensionality (A B: Set)(f: A -> B):
(forall x y:A, I A x y -> I B (f x) (f y)).
Proof.
intros x y P.
induction P.
apply r.
Defined.
(* addition *)
Definition add (m n:N) : N
:= R (fun z=> N) m (fun x y => succ y) n.
(* multiplication *)
Definition mul (m n:N) : N
:= R (fun z=> N) zero (fun x y => add y m) n.
(* Axioms of Peano verified *)
Theorem P1a: (forall x: N, I N (add x zero) x).
intro x.
(* force use of definitional equality
by applying reflexivity *)
apply r.
Defined.
Theorem P1b: (forall x y: N,
I N (add x (succ y)) (succ (add x y))).
intros.
apply r.
Defined.
Theorem P2a: (forall x: N, I N (mul x zero) zero).
intros.
apply r.
Defined.
Theorem P2b: (forall x y: N,
I N (mul x (succ y)) (add (mul x y) x)).
intros.
apply r.
Defined.
Definition pd (n: N): N :=
R (fun _=> N) zero (fun x y=> x) n.
(* alternatively
Definition pd (x: N): N :=
match x as x0 with
| zero => zero
| succ n0 => n0
end.
*)
Theorem P3: (forall x y:N,
I N (succ x) (succ y) -> I N x y).
intros x y p.
apply (I_I_extensionality N N pd (succ x) (succ y)).
apply p.
Defined.
Definition not (A:Set): Set:= (A -> N_0).
Definition isnonzero (n: N): N_2:=
R (fun _ => N_2) zero_2 (fun x y => one_2) n.
Theorem P4 : (forall x:N,
not (I N (succ x) zero)).
intro x.
intro p.
apply (J N (fun x y z =>
Tr (isnonzero x) -> Tr (isnonzero y))
(fun x => (fun t => t)) (succ x) zero)
.
apply p.
simpl.
apply zero_1.
Defined.
Theorem P5 (P:N -> Set):
P zero -> (forall x:N, P x -> P (succ x))
-> (forall x:N, P x).
intros base step n.
apply R.
apply base.
apply step.
Defined.
(* I(A,-,-) is an equivalence relation *)
Lemma Ireflexive (A:Set): (forall x:A, I A x x).
intro x.
apply r.
Defined.
Lemma Isymmetric (A:Set): (forall x y:A, I A x y -> I A y x).
intros x y P.
induction P.
apply r.
Defined.
Lemma Itransitive (A:Set):
(forall x y z:A, I A x y -> I A y z -> I A x z).
intros x y z P Q.
induction P.
assumption.
Defined.
Definition or (A B : Set):= sum' A B.
(* arithmetical expressions *)
Inductive Aexp :Set :=
zer: Aexp
| suc: Aexp -> Aexp
| pls: Aexp -> Aexp -> Aexp.
(* denotation of an expression *)
Definition denotation: Aexp->N:=
fix F (a: Aexp): N :=
match a as a0 with
| zer => zero
| suc a1 => succ (F a1)
| pls a1 a2 => add (F a1) (F a2)
end.
(* predicate for distinguishing
canonical expressions *)
Definition Canonical (x:Aexp):Set :=
or (I Aexp x zer)
(Sigma Aexp (fun y =>
I Aexp x (suc y))).
(* the computation relation is
an inductively defined relation *)
Inductive Comp : Aexp -> Aexp -> Set
:=
refrule: forall a: Aexp,
forall p: Canonical a, Comp a a
| zerrule: forall a b c:Aexp,
forall p: Comp b zer,
forall q: Comp a c,
Comp (pls a b) c
| sucrule: forall a b c:Aexp,
forall p: Comp b (suc c),
Comp (pls a b) (suc (pls a c)).
(* Computations only give canonical
expressions as results *)
Theorem Only_canonical_results:
(forall x y: Aexp, Comp x y -> Canonical y).
admit.
Defined.
(* Here is where help is needed *)
(* Correctness: the computation relation
preserves denotation of expressions *)
Theorem correct_wrt_semantics:
(forall x y: Aexp, Comp x y ->
I N (denotation x) (denotation y)).
admit.
(* Here is where help is need*)
Defined.
(* every input leads to some result *)
Theorem Comp_is_total: (forall x:Aexp,
(Sigma Aexp (fun y =>
prod (Comp x y) (Canonical y)))).
admit.
(* Proof required *)
Defined.
당신이 COQ이 유도 데이터 유형에 대해 자동으로 정의하는'_rect' 제거기에 대해 알고 보인다, 그러나 당신은 그들 모두를 구현할. 교육적인 목적인가? – Ptival
@Ptival 맞음! 저는 Coq를 배우는 중입니다. 따라서 단순히 정의를 가져 오는 대신 정의를 작성하는 것이 좋은 운동이라고 생각했습니다. – user111731