Lazy Evaluation Correctness and Totality (Coq)

Question

As the title suggests, my question concerns proving the correctness and totality of lazy evaluation of arithmetic expressions in Coq. The theorems that I would like to prove are three in total:

1. Computations only give canonical expressions as results

   Theorem Only_canonical_results: (forall x y: Aexp, Comp x y -> Canonical y).

2. 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)).

3. Every input leads to some result.

   Theorem Comp_is_total: (forall x:Aexp, (Sigma Aexp (fun y => prod (Comp x y) (Canonical y)))).

The necessary definitions are to be found in the code attached below. I should make it clear I am a novice when it comes to Coq; which more experienced users will probably notice right away. It is most certainly the case that the majority, or perhaps even all of the background material I have written can be found in the standard library. But, then again, if I knew exactly what to import from the standard library in order to prove the desired results, I would most probably not be here bothering you. That is why I submit to you the material I have so far, in the hope that some kind spirited person/s may help me. Thanks!

(* 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

The first two theorems can be proved almost blindly. They follow by induction on the definition of Comp. The third one requires some thinking and some auxiliary theorems though. But you should be following a tutorial if you want to learn Coq.

About the tactics I used:

• induction 1 does induction on the first unnamed hypothesis.
• info_eauto tries to finish a goal by blindly applying theorems.
• Hint Constructors adds the constructors of an inductive definition to the database of theorems info_eauto can use.
• unfold, simpl, and rewrite should be self-explanatory.

.

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.