Ленивая оценка правильности и целостности (Coq)

Question

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

1. Вычисления дают только канонические выражения как результаты.

   Теорема Only_canonical_results: (в течение x y: Aexp, Comp x y -> Canonical y).

2. Корректность: отношение вычислений сохраняет обозначения выражений

   Теорема correct_wrt_semantics: (для x y: Aexp, Comp x y -> I N (обозначение x) (обозначение y)).

3. Каждый вход приводит к некоторому результату.

   Теорема Comp_is_total: (для всего x:Aexp, (Сигма Aexp (fun y => prod (Comp x y) (Canonical 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.

Answer 1

Первые две теоремы могут быть доказаны почти вслепую. Они следуют по индукции на определение Comp, Третий требует некоторого мышления и некоторых вспомогательных теорем. Но вы должны следовать учебному пособию, если вы хотите изучить Coq.

О тактике, которую я использовал:

• induction 1 делает индукцию по первой неназванной гипотезе.
• info_eauto пытается закончить цель, слепо применяя теоремы.
• Hint Constructors добавляет конструкторы индуктивного определения в базу данных теорем info_eauto можешь использовать.
• unfold, simpl, а также rewrite должно быть само за себя.

,

Hint Constructors sum' prod Sigma I Comp.

Theorem Only_canonical_results:
(forall x y: Aexp, Comp x y -> Canonical y).
unfold Canonical, or.
induction 1.
  info_eauto.
  info_eauto.
  info_eauto.
Defined.

Theorem correct_wrt_semantics:
(forall x y: Aexp, Comp x y -> 
I N (denotation x) (denotation y)).
induction 1.
  info_eauto.
  simpl. rewrite IHComp1. rewrite IHComp2. simpl. info_eauto.
  simpl. rewrite IHComp. simpl. info_eauto.
Defined.

Theorem Comp_is_total: (forall x:Aexp, 
(Sigma Aexp (fun y => 
   prod (Comp x y) (Canonical y)))).
unfold Canonical, or.
induction x.
  eapply Spair. eapply pair.
    eapply refrule. unfold Canonical, or. info_eauto.
    info_eauto.
Admitted.