(*** Semantics, Coq part of Assignment 7 ***) (*** Use Coq to complete the file below. If you have any questions, please use the discussion board. http://www.ps.uni-saarland.de/courses/sem-ws13-forum ***) Require Import Base ARS. Set Implicit Arguments. Unset Strict Implicit. (** * Definitions *) Notation "R '<=1' S" := (forall x, R x -> S x) (at level 70). Notation "R '<=2' S" := (forall x y, R x y -> S x y) (at level 70). Notation "R '=1' S" := (R <=1 S /\ S <=1 R) (at level 70). Notation "R '=2' S" := (R <=2 S /\ S <=2 R) (at level 70). Notation "p /\1 q" := (fun x => p x /\ q x) (at level 50). (** Exercise 7.4 *) Definition NS := S. (** * CL terms and one step reduction *) Inductive term := Var (x : nat) | K | S | App (s t : term). Coercion App : term >-> Funclass. Inductive step : term -> term -> Prop := | stepK s t : step (K s t) s | stepS s t u : step (S s t u) (s u (t u)) | stepAL s s' t : step s s' -> step (s t) (s' t) | stepAR (s : term) t t' : step t t' -> step (s t) (s t'). (** * CL reduction is decidable *) Fixpoint redex (s : term) : bool := match s with | App (App K _) _ | App (App (App S _) _) _ => true | _ => false end. Inductive termi : term -> Type := | termiV x : termi (Var x) | termiK : termi K | termiS : termi S | termiRK s t : termi s -> termi t -> termi (K s t) | termiRS s t u : termi s -> termi t -> termi u -> termi (S s t u) | termiA s t : redex (App s t) = false -> termi s -> termi t -> termi (s t). Lemma term_to_termi s : termi s. Proof. (*** FILL IN HERE ***) Admitted. Lemma step_classical s : dec (reducible step s). Proof. (*** FILL IN HERE ***) Admitted. (** * Confluence *) Inductive pstep : term -> term -> Prop := | pstepK s s' t : pstep s s' -> pstep (K s t) s' | pstepS s s' t t' u u' : pstep s s' -> pstep t t' -> pstep u u' -> pstep (S s t u) (s' u' (t' u')) | pstepA s s' t t' : pstep s s' -> pstep t t' -> pstep (s t) (s' t') | pstepRV x : pstep (Var x) (Var x) | pstepRK : pstep K K | pstepRS : pstep S S. Fixpoint rho (s : term) : term := match s with | App (App K s) t => rho s | App (App (App S s) t) u => rho s (rho u) (rho t (rho u)) | App s t => (rho s) (rho t) | s => s end. Lemma pstep_refl : reflexive pstep. Proof. (*** FILL IN HERE ***) Admitted. Lemma step_pstep : step <=2 pstep. Proof. (*** FILL IN HERE ***) Admitted. Lemma red_app s s' t t' : star step s s' -> star step t t' -> star step (s t) (s' t'). Proof. (*** FILL IN HERE ***) Admitted. Lemma pstep_step : pstep <=2 star step. Proof. (*** FILL IN HERE ***) Admitted. Lemma star_step_star_pstep : star step =2 star pstep. Proof. (*** FILL IN HERE ***) Admitted. Lemma triangle_to_CR : triangle pstep rho -> church_rosser step. Proof. (*** FILL IN HERE ***) Admitted. Lemma rho_triangle : triangle pstep rho. Proof. (*** FILL IN HERE ***) Admitted. Theorem CL_is_CR : church_rosser step. Proof. apply triangle_to_CR, rho_triangle. Qed.