Module combinators

This Coq module contains a formalization of the computation model based on the combinators K and S. We define an inductive datatype for programs and an inductive reduction relation to express the small-step semantics.

The main result of this module is the confluence of the calculus. It contains also the corollary which says that each term has at most one normal form.

(Vincent Cremet - mars 2003 - Coq-7.4)

The terms of the calculus.

Inductive Term: Set := K: Term | S: Term | app: Term -> Term -> Term.

One step reduction relation.

Inductive one_step: Term -> Term -> Prop := redk: (m, n: Term) (one_step (app (app K m) n) m) | reds: (m, n, p: Term) (one_step (app (app (app S m) n) p) (app (app m p) (app n p))) | redl: (m, m', n: Term) (one_step m m') -> (one_step (app m n) (app m' n)) | redr: (m, n, n': Term) (one_step n n') -> (one_step (app m n) (app m n')).

Transitive, reflexive closure of a relation.

Inductive trclosure[A: Set; reduce: A -> A -> Prop] : A -> A -> Prop := trcl_refl: (m: A) (trclosure A reduce m m) | trcl_trans: (m, n: A) (trclosure A reduce m n) -> (p: A) (trclosure A reduce n p) -> (trclosure A reduce m p) | trcl_step: (m, n: A) (reduce m n) -> (trclosure A reduce m n).

Transitive reflexive closure is monotonic (unused in the confluence proof).

Lemma trcl_monotonic: (A: Set; rel1, rel2: A -> A -> Prop) ((m, n: A) (rel1 m n) -> (rel2 m n)) -> ((m, n: A) (trclosure A rel1 m n) -> (trclosure A rel2 m n)). Intros. NewInduction H0.

Apply trcl_refl.

Apply trcl_trans with n. Trivial. Trivial.

Apply trcl_step. Apply H. Trivial. Qed.

Reflexive closure of a relation.

Inductive rclosure[A: Set; red: A -> A -> Prop] : A -> A -> Prop := rcl_refl: (m: A) (rclosure A red m m) | rcl_step: (m, n: A) (red m n) -> (rclosure A red m n).

The transitive reflexive closure of the reflexive closure of a relation is the transitive reflexive closure of the relation (not used in the confluence proof).

Lemma tr_rcl_is_trcl: (A: Set) (rel: A -> A -> Prop) (m, n: A) ((trclosure A (rclosure A rel) m n) <-> (trclosure A rel m n)).

Intros. Split. Intro. NewInduction H. Apply trcl_refl. Apply trcl_trans with n. Trivial. Trivial. NewInduction H. Apply trcl_refl. Apply trcl_step. Trivial.

Intro. NewInduction H. Apply trcl_refl. Apply trcl_trans with n. Trivial. Trivial. Apply trcl_step. Apply rcl_step. Trivial. Qed.

General reduction.

Definition reduce := (trclosure Term one_step).

Lemma reduce_left: (m, m': Term) (reduce m m') -> (n: Term) (reduce (app m n) (app m' n)).

Intros m m' H. NewInduction H. Intro. Unfold reduce. Apply trcl_refl.

Intro. Unfold reduce. Apply trcl_trans with (app n n0). Apply IHtrclosure1. Apply IHtrclosure2.

Intro. Unfold reduce. Apply trcl_step. Apply redl. Trivial. Qed.

Lemma reduce_right: (m, m': Term) (reduce m m') -> (n: Term) (reduce (app n m) (app n m')).

Intros m m' H. NewInduction H. Intro. Unfold reduce. Apply trcl_refl.

Intro. Unfold reduce. Apply trcl_trans with (app n0 n). Apply IHtrclosure1. Apply IHtrclosure2.

Intro. Unfold reduce. Apply trcl_step. Apply redr. Trivial. Qed.

The diamond property for a binary relation.

Definition diamond [A: Set; reduce: A -> A -> Prop]: Prop := (m, n1: A) (reduce m n1) -> (n2: A) (reduce m n2) -> (EX p: A | (reduce n1 p) /\ (reduce n2 p)) .

Definition of the confluence of the calculus.

Definition confluence: Prop := (diamond Term reduce).

Definition of the concept of computation of a result by a term.

Definition computes [m, n: Term]: Prop := (reduce m n) /\ (p: Term) ~(one_step n p).

Parallel reduction (needed for the proof of confluence).

Inductive par_step: Term -> Term -> Prop := par_refl: (m: Term) (par_step m m ) | park: (m, m', n, n': Term) (par_step m m') -> (par_step n n') -> (par_step (app (app K m) n) m') | pars: (m, m', n, n', p, p': Term) (par_step m m') -> (par_step n n') -> (par_step p p') -> (par_step (app (app (app S m) n) p) (app (app m' p') (app n' p'))) | parapp: (m, m', n, n': Term) (par_step m m') -> (par_step n n') -> (par_step (app m n) (app m' n')).

The diamond property is preserved by reflexive, transitive closure.

Lemma diamond_trcl: (A: Set; reduce: A -> A -> Prop) (diamond A reduce) -> (diamond A (trclosure A reduce)).

Assert cl_diamond1: (A: Set; red: A -> A -> Prop) (diamond A red) -> (m, n1: A) (trclosure A red m n1) ->(n2: A) (red m n2) -> (EX p: A | (red n1 p) /\ (trclosure A red n2 p)).

Intros A red D m n1 H. NewInduction H. Intros. Exists n2. Split. Trivial. Apply trcl_refl.

Intros. Case (IHtrclosure1 n2 H0). Intros. Case (IHtrclosure2 x (proj1 ?? H2)). Intros. Exists x0. Split. Tauto. Apply trcl_trans with x. Tauto. Tauto.

Intros. Unfold diamond in D. Case (D ?? H ? H0). Intros. Exists x. Split. Tauto. Apply trcl_step. Tauto. Intros A reduce0 H. Unfold diamond. Intros m n1 H0. NewInduction H0.

Intros. Exists n2. Split. Trivial. Apply trcl_refl.

Clear H. Intros. Assert (EX q: A | (trclosure A reduce0 n q) /\(trclosure A reduce0 n2 q)). Apply IHtrclosure1. Trivial. Case H2. Clear H2. Intros. Assert (EX q: A | (trclosure A reduce0 p q) /\(trclosure A reduce0 x q)). Apply IHtrclosure2. Tauto. Case H3. Clear H3. Intros. Exists x0. Split. Tauto. Apply trcl_trans with x. Tauto. Tauto.

Intros. Case (cl_diamond1 ?? H m n2 H1 n H0). Intros. Exists x. Split. Tauto. Apply trcl_step. Tauto. Qed.

The parallel reduction relation is included in the general reduction relation.

Lemma par_sub_reduce: (m, n: Term) (par_step m n) -> (reduce m n).

Intros. NewInduction H.

Unfold reduce. Apply trcl_refl.

Unfold reduce. Apply trcl_trans with (app (app K m') n). Apply reduce_left. Apply reduce_right. Trivial. Apply trcl_step. Apply redk.

Unfold reduce. Apply trcl_trans with (app (app (app S m') n) p). Apply reduce_left. Apply reduce_left. Apply reduce_right. Trivial. Apply trcl_trans with (app (app (app S m') n') p). Apply reduce_left. Apply reduce_right. Trivial. Apply trcl_trans with (app (app (app S m') n') p'). Apply reduce_right. Trivial. Apply trcl_step. Apply reds.

Unfold reduce. Apply trcl_trans with (app m' n). Apply reduce_left. Trivial. Apply trcl_trans with (app m' n'). Apply reduce_right. Trivial. Apply trcl_refl. Qed.

The one-step reduction relation is included in the parallel reduction relation.

Lemma onestep_sub_par: (m, n: Term) (one_step m n) -> (par_step m n).

Intros. NewInduction H. Apply park with n. Apply par_refl. Apply par_refl. Apply pars. Apply par_refl. Apply par_refl. Apply par_refl. Apply parapp. Trivial. Apply par_refl. Apply parapp. Apply par_refl. Trivial. Qed.

The transitive reflexive closure of the parallel reduction relation coincides with the general reduction relation.

Lemma parstar_is_reduce: (m, n: Term) ((trclosure Term par_step m n) <-> (reduce m n)).

Intros. Split. Intro. NewInduction H.

Unfold reduce. Apply trcl_refl.

Unfold reduce. Apply trcl_trans with n. Trivial. Trivial. Apply par_sub_reduce. Trivial.

Intro. NewInduction H.

Apply trcl_refl. Apply trcl_trans with n. Trivial. Trivial. Apply trcl_step. Apply onestep_sub_par. Trivial. Qed.

In some cases we can deduce informations on the shape of a reduced term.

Lemma km: (m, n: Term) (par_step (app K m) n) -> (EX m': Term | (n = (app K m')) /\ (par_step m m')).

Assert km_tmp: (m, n: Term) (par_step m n) -> (p: Term) (m = (app K p)) -> (EX p': Term | (n = (app K p')) /\ (par_step p p')).

Intros m n H. Case H.

Intros. Exists p. Split. Trivial. Apply par_refl.

Intros. Discriminate H2.

Intros. Discriminate H3.

Intros. Exists n'. Injection H2. Intros. Replace p with n0. Assert m' = K. Assert (par_step K m'). Replace K with m0. Trivial.

Assert (m, n: Term) (par_step m n) -> (m = K) -> (n = K). Intros m1 n1 V. Case V. Tauto. Intros. Discriminate H8. Intros. Discriminate H9. Intros. Discriminate H8.

Apply H6 with m0. Trivial. Trivial. Replace m' with K. Tauto. Intros. Apply km_tmp with (app K m). Trivial. Reflexivity. Qed.

Lemma sm: (m, n: Term) (par_step (app S m) n) -> (EX m': Term | (n = (app S m')) /\ (par_step m m')).

Assert sm_tmp: (m, n: Term) (par_step m n) -> (p: Term) (m = (app S p)) -> (EX p': Term | (n = (app S p')) /\ (par_step p p')).

Intros m n H. Case H.

Intros. Exists p. Split. Trivial. Apply par_refl.

Intros. Discriminate H2.

Intros. Discriminate H3.

Intros. Exists n'. Injection H2. Intros. Replace p with n0. Assert m' = S. Assert (par_step S m'). Replace S with m0. Trivial.

Assert (m, n: Term) (par_step m n) -> (m = S) -> (n = S). Intros m1 n1 V. Case V. Tauto. Intros. Discriminate H8. Intros. Discriminate H9. Intros. Discriminate H8.

Apply H6 with m0. Trivial. Trivial. Replace m' with S. Tauto. Intros. Apply sm_tmp with (app S m). Trivial. Reflexivity. Qed.

Lemma smn: (m, n, p: Term) (par_step (app (app S m) n) p) -> (EX m': Term | (EX n': Term | (p = (app (app S m') n')) /\ (par_step m m') /\ (par_step n n'))).

Assert smn_tmp: (m, n: Term) (par_step m n) -> (p, q: Term) (m = (app (app S p) q)) -> (EX p': Term | (EX q': Term | (n = (app (app S p') q')) /\ (par_step p p') /\ (par_step q q'))).

Intros m n H. Case H. Intros. Exists p. Exists q. Split. Trivial. Split. Apply par_refl. Apply par_refl. Intros. Discriminate H2. Intros. Discriminate H3. Intros. Injection H2. Intros. Clear H2.

Assert (par_step (app S p) m'). Replace (app S p) with m0. Trivial. Case (sm p m' H2). Clear H2. Intros.

Exists x. Exists n'. Replace m' with (app S x). Split. Reflexivity. Split. Tauto. Replace q with n0. Trivial. Apply sym_eq. Tauto. Intros. Apply smn_tmp with (app (app S m) n). Trivial. Reflexivity. Qed.

Different ways for an application to reduce.

Lemma decompose: (m1, m2, n: Term) (par_step (app m1 m2) n) -> (n = (app m1 m2)) \/ (EX l | (EX l' | (EX m2' | m1 = (app K l) /\ (par_step l l') /\ (par_step m2 m2') /\ (n = l')))) \/ (EX l1 | (EX l2 | (EX l1' | (EX l2' | (EX m2' | m1 = (app (app S l1) l2) /\ (par_step l1 l1') /\ (par_step l2 l2') /\ (par_step m2 m2') /\ (n = (app (app l1' m2') (app l2' m2')))))))) \/ (EX m1': Term | (EX m2': Term | (par_step m1 m1') /\ (par_step m2 m2') /\ (n = (app m1' m2')))).

Assert decompose_tmp: (m, n: Term) (par_step m n) -> (m1, m2: Term) (m = (app m1 m2)) -> (n = (app m1 m2)) \/ (EX l | (EX l' | (EX m2' | m1 = (app K l) /\ (par_step l l') /\ (par_step m2 m2') /\ (n = l')))) \/ (EX l1 | (EX l2 | (EX l1' | (EX l2' | (EX m2' | m1 = (app (app S l1) l2) /\ (par_step l1 l1') /\ (par_step l2 l2') /\ (par_step m2 m2') /\ (n = (app (app l1' m2') (app l2' m2')))))))) \/ (EX m1': Term | (EX m2': Term | (par_step m1 m1') /\ (par_step m2 m2') /\ (n = (app m1' m2')))).

Intros m n V. Case V. Intros. Left. Trivial.

Intros. Right. Left. Injection H1. Intros. Exists m0. Exists m'. Exists n'. Replace m2 with n0. Split. Apply sym_eq. Trivial. Split. Tauto. Tauto.

Intros. Right. Right. Left. Injection H2. Intros. Exists m0. Exists n0. Exists m'. Exists n'. Exists p'. Split. Apply sym_eq. Trivial. Split. Trivial. Split. Trivial. Split. Replace m2 with p. Trivial. Reflexivity.

Intros. Injection H1. Intros. Right. Right. Right. Exists m'. Exists n'. Replace m1 with m0. Replace m2 with n0. Tauto. Intros. Apply decompose_tmp with (app m1 m2). Trivial. Reflexivity. Qed.

Parallel reduction satisfies the diamond property.

Theorem diamond_par_step: (diamond Term par_step).

Unfold diamond. Intro m. NewInduction m.

Intros. Exists n2. Assert n1 = K.

Assert (m, n: Term) (par_step m n) -> (m = K) -> (n = K). Intros m n V. Case V. Intros. Trivial. Intros. Discriminate H3. Intros. Discriminate H4. Intros. Discriminate H3.

Apply H1 with K. Trivial. Reflexivity. Replace n1 with K. Split. Trivial. Apply par_refl.

Intros. Exists n2. Assert n1 = S.

Assert (m, n: Term) (par_step m n) -> (m = S) -> (n = S). Intros m n V. Case V. Intros. Trivial. Intros. Discriminate H3. Intros. Discriminate H4. Intros. Discriminate H3.

Apply H1 with S. Trivial. Reflexivity. Replace n1 with S. Split. Trivial. Apply par_refl.

Intros.

Case (decompose m1 m2 n1 H). Intro. Exists n2. Replace n1 with (app m1 m2). Split. Trivial. Apply par_refl.

Intro. Case H1. Clear H1. Intro. Case H1. Clear H1. Intros. Case H1. Clear H1. Intros. Case H1. Clear H1. Intros.

Case (decompose m1 m2 n2 H0). Intro. Exists n1. Split. Apply par_refl. Replace n2 with (app m1 m2). Trivial.

Intro.

Case H2. Clear H2. Intro. Case H2. Clear H2. Intros. Case H2. Clear H2. Intros. Case H2. Clear H2. Intros. Assert (par_step m1 (app K x0)). Replace m1 with (app K x). Apply parapp. Apply par_refl. Tauto. Apply sym_eq. Tauto. Assert (par_step m1 (app K x3)). Replace m1 with (app K x2). Apply parapp. Apply par_refl. Tauto. Apply sym_eq. Tauto. Case (IHm1 (app K x0) H3 (app K x3) H4). Intros. Case (km ? ? (proj1 ?? H5)). Intros. Case (km ? ? (proj2 ?? H5)). Intros. Assert (app K x6) = (app K x7). Replace (app K x6) with x5. Replace (app K x7) with x5. Reflexivity. Tauto. Tauto. Injection H8. Clear H8. Intro. Assert (par_step x3 x6). Replace x6 with x7. Tauto. Exists x6. Replace n1 with x0. Replace n2 with x3. Tauto. Apply sym_eq. Tauto. Apply sym_eq. Tauto.

Intro. Clear H2. Case H3. Clear H3. Intro. Case H2. Clear H2. Intros. Case H2. Clear H2. Intros. Case H2. Clear H2. Intros. Case H2. Clear H2. Intros. Case H2. Clear H2. Intros. Assert ((app K x) = (app (app S x2) x3)). Replace (app K x) with m1. Replace (app (app S x2) x3) with m1. Reflexivity. Tauto. Tauto. Discriminate H3.

Clear H3. Intro. Case H2. Clear H2. Intros. Case H2. Clear H2. Intros. Case (IHm2 x1 (proj1 ?? (proj2 ?? (proj2 ?? H1))) x3 (proj1 ?? (proj2 ?? H2))). Intros. Assert (par_step (app K x) x2). Replace (app K x) with m1. Tauto. Tauto. Case (km ? ? H4). Clear H4. Intros. Assert (par_step m1 (app K x5)). Replace (app K x5) with x2. Tauto. Tauto. Assert (par_step m1 (app K x0)). Replace m1 with (app K x). Apply parapp. Apply par_refl. Tauto. Apply sym_eq. Tauto. Case (IHm1 (app K x0) H6 (app K x5) H5). Intros. Clear IHm1. Clear IHm2. Case (km ?? (proj1 ?? H7)). Intros. Case (km ?? (proj2 ?? H7)). Intros. Exists x7. Replace n1 with x0. Split. Tauto. Replace n2 with (app x2 x3). Replace x2 with (app K x5). Replace x7 with x8. Apply park with x3. Tauto. Apply par_refl. Assert ((app K x8) = (app K x7)). Replace (app K x8) with x6. Replace (app K x7) with x6. Reflexivity. Tauto. Tauto. Injection H10. Tauto. Apply sym_eq ; Tauto. Apply sym_eq ; Tauto. Apply sym_eq ; Tauto.

Clear H1. Intro. Case H1. Clear H1. Intro. Case H1. Clear H1. Intros. Case H1. Clear H1. Intros. Case H1. Clear H1. Intros. Case H1. Clear H1. Intros. Case H1. Clear H1. Intros.

Case (decompose m1 m2 n2 H0). Intro. Exists n1. Split. Apply par_refl. Replace n2 with (app m1 m2). Tauto. Intro.

Case H2. Clear H2. Intro. Case H2. Clear H2. Intros. Case H2. Clear H2. Intros. Case H2. Clear H2. Intros. Assert ((app (app S x) x0) = (app K x4)). Replace (app (app S x) x0) with m1. Replace (app K x4) with m1. Reflexivity. Tauto. Tauto. Discriminate H3.

Clear H2. Intro. Case H2. Clear H2. Intro. Case H2. Clear H2. Intros. Case H2. Clear H2. Intros. Case H2. Clear H2. Intros. Case H2. Clear H2. Intros. Case H2. Clear H2. Intros. Assert ((app (app S x) x0) = (app (app S x4) x5)). Replace (app (app S x) x0) with m1. Replace (app (app S x4) x5) with m1. Reflexivity. Tauto. Tauto. Injection H3. Clear H3. Intros. Case (IHm2 x3 (proj1 ?? (proj2 ?? (proj2 ?? (proj2 ?? H1)))) x8 (proj1 ?? (proj2 ?? (proj2 ?? (proj2 ?? H2))))). Clear IHm2. Intros. Assert (par_step m1 (app (app S x1) x2)). Replace m1 with (app (app S x) x0). Apply parapp. Apply parapp. Apply par_refl. Tauto. Tauto. Apply sym_eq; Tauto. Assert (par_step m1 (app (app S x6) x7)). Replace m1 with (app (app S x) x0). Replace x with x4. Replace x0 with x5. Apply parapp. Apply parapp. Apply par_refl. Tauto. Tauto. Apply sym_eq; Tauto. Case (IHm1 (app (app S x1) x2) H6 (app (app S x6) x7) H7). Clear H6. Clear H7. Intros. Case (smn x1 x2 x10 (proj1 ?? H6)). Intros. Case (smn x6 x7 x10 (proj2 ?? H6)). Clear H6. Intros. Case H7. Clear H7. Case H6. Clear H6. Intros. Exists (app (app x12 x9) (app x13 x9)). Replace n1 with (app (app x1 x3) (app x2 x3)). Replace n2 with (app (app x6 x8) (app x7 x8)). Assert ((app (app S x12) x13) = (app (app S x11) x14)). Apply trans_eq with x10. Apply sym_eq; Tauto. Tauto. Injection H8. Clear H8. Intros. Split. Replace x12 with x11. Replace x13 with x14. Apply parapp. Apply parapp. Tauto. Tauto. Apply parapp. Tauto. Tauto. Apply parapp. Apply parapp; Tauto. Apply parapp; Tauto. Apply sym_eq; Tauto. Apply sym_eq; Tauto.

Clear H2. Intros. Case H2. Clear H2. Intros. Case H2. Clear H2. Intros.

Assert (par_step (app (app S x) x0) x4). Replace (app (app S x) x0) with m1; Tauto. Case (smn x x0 x4 H3). Intros. Case H4. Clear H4. Intros.

Assert (par_step m1 (app (app S x6) x7)). Replace (app (app S x6) x7) with x4; Tauto. Assert (par_step m1 (app (app S x1) x2)). Replace m1 with (app (app S x) x0). Apply parapp. Apply parapp. Apply par_refl; Tauto. Tauto. Tauto. Apply sym_eq; Tauto. Case (IHm1 (app (app S x6) x7) H5 (app (app S x1) x2) H6). Clear IHm1. Intros. Case (smn x6 x7 x8 (proj1 ?? H7)). Case (smn x1 x2 x8 (proj2 ?? H7)). Clear H7. Intros. Case H7. Clear H7. Case H8. Clear H8. Intros. Assert ((app (app S x10) x11) = (app (app S x9) x12)). Apply trans_eq with x8. Apply sym_eq; Tauto. Tauto. Injection H9. Clear H9. Intros.

Case (IHm2 x3 (proj1 ?? (proj2 ?? (proj2 ?? (proj2 ?? H1)))) x5 (proj1 ?? (proj2 ?? H2))). Clear IHm2. Intros.

Exists (app (app x9 x13) (app x11 x13)). Split. Replace n1 with (app (app x1 x3) (app x2 x3)). Apply parapp. Apply parapp. Tauto. Tauto. Apply parapp. Replace x11 with x12. Tauto. Tauto. Apply sym_eq; Tauto.

Replace n2 with (app x4 x5). Replace x4 with (app (app S x6) x7). Apply pars. Replace x9 with x10. Tauto. Tauto. Tauto. Apply sym_eq; Tauto. Apply sym_eq; Tauto.

Clear H1. Intro. Case H1. Clear H1. Intros. Case H1. Clear H1. Intros.

Case (decompose m1 m2 n2 H0).

Intro. Exists n1. Split. Apply par_refl. Replace n2 with (app m1 m2). Tauto.

Intro. Case H2. Clear H2. Intros. Case H2. Clear H2. Intros. Case H2. Clear H2. Intros. Case H2. Clear H2. Intros.

Assert (par_step (app K x1) x). Replace (app K x1) with m1. Tauto. Tauto. Case (km x1 x H3). Clear H3. Intros.

Assert (par_step m1 (app K x4)). Replace (app K x4) with x. Tauto. Tauto. Assert (par_step m1 (app K x2)). Replace m1 with (app K x1). Apply parapp. Apply par_refl. Tauto. Apply sym_eq; Tauto. Clear IHm2. Case (IHm1 (app K x4) H4 (app K x2) H5). Clear H4. Clear H5. Intros. Case (km x4 x5 (proj1 ?? H4)). Case (km x2 x5 (proj2 ?? H4)). Clear H4. Intros. Assert ((app K x6) = (app K x7)). Apply trans_eq with x5. Apply sym_eq; Tauto. Tauto. Injection H6. Clear H6. Intro. Exists x6.

Replace n1 with (app x x0). Replace x with (app K x4). Replace n2 with x2. Split. Apply park with x0. Replace x6 with x7. Tauto. Apply par_refl. Tauto. Apply sym_eq; Tauto. Apply sym_eq; Tauto. Apply sym_eq; Tauto.

Clear H2. Intros. Case H2. Clear H2. Intros. Case H2. Clear H2. Intros. Case H2. Clear H2. Intros. Case H2. Clear H2. Intros. Case H2. Clear H2. Intros. Case H2. Clear H2. Intros.

Assert (par_step (app (app S x1) x2) x). Replace (app (app S x1) x2) with m1; Tauto. Case (smn x1 x2 x H3). Intros. Case H4. Clear H4. Intros.

Assert (par_step m1 (app (app S x6) x7)). Replace (app (app S x6) x7) with x; Tauto. Assert (par_step m1 (app (app S x3) x4)). Replace m1 with (app (app S x1) x2). Apply parapp. Apply parapp. Apply par_refl; Tauto. Tauto. Tauto. Apply sym_eq; Tauto. Case (IHm1 (app (app S x6) x7) H5 (app (app S x3) x4) H6). Clear IHm1. Intros. Case (smn x6 x7 x8 (proj1 ?? H7)). Case (smn x3 x4 x8 (proj2 ?? H7)). Clear H7. Intros. Case H7. Clear H7. Case H8. Clear H8. Intros. Assert ((app (app S x10) x11) = (app (app S x9) x12)). Apply trans_eq with x8. Apply sym_eq; Tauto. Tauto. Injection H9. Clear H9. Intros.

Case (IHm2 x5 (proj1 ?? (proj2 ?? (proj2 ?? (proj2 ?? H2)))) x0 (proj1 ?? (proj2 ?? H1))). Clear IHm2. Intros.

Exists (app (app x9 x13) (app x11 x13)). Split. Replace n1 with (app x x0). Replace x with (app (app S x6) x7). Apply pars. Replace x9 with x10. Tauto. Tauto. Tauto. Apply sym_eq; Tauto. Apply sym_eq; Tauto. Replace n2 with (app (app x3 x5) (app x4 x5)). Apply parapp. Apply parapp. Tauto. Tauto. Apply parapp. Replace x11 with x12. Tauto. Tauto. Apply sym_eq; Tauto.

Clear H2. Intro. Case H2. Clear H2. Intros. Case H2. Clear H2. Intros.

Case (IHm1 x (proj1 ?? H1) x1 (proj1 ?? H2)). Clear IHm1. Case (IHm2 x0 (proj1 ?? (proj2 ?? H1)) x2 (proj1 ?? (proj2 ?? H2))). Clear IHm2. Intros. Exists (app x4 x3). Replace n1 with (app x x0). Replace n2 with (app x1 x2). Split. Apply parapp. Tauto. Tauto. Apply parapp. Tauto. Tauto. Apply sym_eq; Tauto. Apply sym_eq; Tauto. Qed.

Diamond property is substitutive.

Lemma substDiamond: (A: Set)(rel1, rel2: A -> A -> Prop) ((m, n: A) ((rel1 m n) <-> (rel2 m n))) -> (diamond A rel1) -> (diamond A rel2).

Unfold diamond. Intros. Assert (rel1 m n1). Assert (rel1 m n1)<->(rel2 m n1). Exact (H m n1). Tauto. Assert (rel1 m n2). Assert (rel1 m n2)<->(rel2 m n2). Exact (H m n2). Tauto. Case (H0 m n1 H3 n2 H4). Intros. Exists x. Split. Assert (rel1 n1 x)<->(rel2 n1 x). Apply H. Tauto. Assert (rel1 n2 x)<->(rel2 n2 x). Apply H. Tauto. Qed.

The calculus of combinators K and S is confluent.

Theorem pConfluence: confluence.

Unfold confluence. Apply substDiamond with (trclosure Term par_step). Exact parstar_is_reduce. Apply diamond_trcl. Exact diamond_par_step. Qed.

A stuck term can only reduce to itself.

Lemma pStuck: (m, n: Term) (reduce m n) -> ((p: Term) ~(one_step m p)) -> (m = n). Intros m n H. NewInduction H. Reflexivity. Intros. Assert m = n. Tauto. Replace m with n. Apply IHtrclosure2. Replace n with m. Trivial. Intro. Assert False. Apply (H0 n). Trivial. Tauto. Qed.

The relation which results to programs is in fact a function.

Lemma pComputes: (m, n1, n2: Term) (computes m n1) -> (computes m n2) -> (n1 = n2). Intros. Unfold computes in H. Unfold computes in H0. Case (pConfluence ?? (proj1 ?? H) ? (proj1 ?? H0)). Intros. Assert n1 = x. Apply (pStuck ?? (proj1 ?? H1) (proj2 ?? H)). Assert n2 = x. Apply (pStuck ?? (proj2 ?? H1) (proj2 ?? H0)). Replace n1 with x. Replace n2 with x. Reflexivity. Qed.

Index

This page has been generated by coqdoc