Require Import mathcomp.ssreflect.ssreflect. (* Reduction theory *) (* Type of relations *) Definition Rel (A B:Type) := A -> B -> Prop. (* Type of reduction relations *) Definition Red (A:Type) := Rel A A. (* Inclusion of a relation in another relation *) Definition Sub {A B} (R1 R2: Rel A B) : Prop := forall a b, R1 a b -> R2 a b. Notation "R1 <# R2" := (Sub R1 R2) (at level 50). (* Inclusion is reflexive *) Lemma SubRefl {A B} (R: Rel A B) : R <# R. Proof. done. Qed. (* Inclusion is transitive *) Lemma SubTrans {A B} (R2 R1 R3: Rel A B) : R1 <# R2 -> R2 <# R3 -> R1 <# R3. Proof. rewrite/Sub. auto. Qed. (* Double inclusion, i.e. equivalence *) Definition Equiv {A B} (R1 R2: Rel A B) := R1 <# R2 /\ R2 <# R1. Notation "R1 -- R2" := (Equiv R1 R2) (at level 50). (* Composition of relations *) Inductive comp {A B C} (red1: Rel A B)(red2: Rel B C) : Rel A C := compose: forall b a c, red1 a b -> red2 b c -> comp red1 red2 a c . Notation "R1 # R2" := (comp R1 R2) (at level 40). Arguments compose {A B C red1 red2} _ _ _ _ _ . (* Inverse of a relation *) Inductive inverse {A B} (R: Rel A B) : Rel B A := inverseof: forall a b, R a b -> inverse R b a . (* Composition is associative *) Lemma compTrans {A B C D} (R1: Rel A B)(R2: Rel B C)(R3: Rel C D) : (R1 # R2) # R3 -- R1 # (R2 # R3). Proof. rewrite /Equiv; split. rewrite/Sub. move => a b H. inversion H. inversion H0. apply (compose b1) => //. apply (compose b0) => //. rewrite/Sub. move => a b H. inversion H. inversion H1. apply (compose b1) => //. apply (compose b0) => //. Qed. (* Composition is monotonous *) Lemma SubComp {A B C} (R1 R2: Rel A B)(R3 R4: Rel B C) : R1 <# R2 -> R3 <# R4 -> (comp R1 R3) <# (comp R2 R4). Proof. rewrite/Sub. move => H1 H2 a b; elim => a0 b0 c0 H3 H4. apply (compose a0). auto. auto. Qed. (* Transitive closure of a reduction relation *) Inductive trans {A} (red: Red A) : Red A := | singl: forall a b, red a b -> trans red a b | transit: forall b a c, red a b -> trans red b c -> trans red a c . Arguments transit {A} {red} _ _ _ _ _ . (* A reduction relation is included in its transitive closure *) Lemma transSub {A:Type} (red: Red A) : red <# (trans red). Proof. rewrite /Sub. move => a b H. apply singl => //. Qed. (* Given a path from a to b and a path from b to c, construction of the path from a to c *) Lemma tailtransit {A red}: forall (b a c:A), trans red a b -> trans red b c -> trans red a c. Proof. move => a b c H1 H2. induction H1. apply (transit b) =>//. apply (transit b) =>//. apply IHtrans =>//. Qed. (* Transitive closure is monotonous *) Lemma SubTrans1 {A} (red1 red2: Red A) : red1 <# red2 -> (trans red1) <# (trans red2). Proof. rewrite /Sub => H a b H0. induction H0. apply singl. auto. apply (transit b) => //. auto. Qed. (* Image of a predicate via a relation *) Inductive Image {A B} (R:Rel A B)(P: A -> Prop): B -> Prop := image: forall a b, P a -> R a b -> Image R P b. Arguments image {A B R P} _ _ _ _. (***************) (* Simulations *) (* Strong simulation: redA is strongly simulated by redB through R (one step of redA yields at least one step of redB) *) Definition StrongSimul {A B} (redA: Red A) (redB: Red B) (R: Rel A B) := ((inverse R) # redA) <# ((trans redB) # (inverse R)). (* The fact that redA is strongly simulated by redB is monotonic in redB and anti-monotonic in redA *) Lemma SimulMonotonic {A B} (redA1 redA2: Red A) (redB1 redB2: Red B) (R: Rel A B): redA2 <# redA1 -> redB1 <# redB2 -> StrongSimul redA1 redB1 R -> StrongSimul redA2 redB2 R. Proof. move => H1 H2. rewrite /StrongSimul. move => H3. apply (SubTrans ((inverse R) # redA1)). apply SubComp =>//. apply (SubTrans ((trans redB1) # (inverse R))) => //. apply SubComp =>//. apply SubTrans1 => //. Qed. (* If redA1 and redA2 are strongly simulated by the same relation, so is their composition *) Lemma SimulBoth {A B} (redA1 redA2: Red A) (redB: Red B) (R: Rel A B): StrongSimul redA1 redB R -> StrongSimul redA2 redB R -> StrongSimul (redA1 # redA2) redB R. Proof. rewrite /StrongSimul. move => H1 H2. rewrite/Sub => a b H3. inversion H3; clear H3. clear H4 H5 a0 c. inversion H0; clear H0. clear H5 H6 a0 c. rewrite /Sub in H1. have: ((inverse R # redA1) a b1). apply: (compose b0) =>//. move => H5; move: (H1 a b1 H5); clear H1 => H1. inversion H1; clear H1. clear H7 H8 H5 a0 c. have: ((inverse R # redA2) b2 b). apply: (compose b1) =>//. move => H5; move: (H2 _ _ H5); clear H2 => H2. inversion H2; clear H2. clear H9 H8 H5 a0 c. apply: (compose b3) =>//. apply: (tailtransit b2) => //. Qed. (* If redA is strongly simulated, so is its transitive closure *) Lemma SimulTrans {A B} (redA: Red A) (redB: Red B) (R: Rel A B) : StrongSimul redA redB R -> StrongSimul (trans redA) redB R. Proof. rewrite /StrongSimul. move => H. rewrite/Sub => b a H0. inversion H0. clear H3 H4 a0 c H0. move : b H1. induction H2. move => b0 H1. rewrite /Sub in H. have : ((inverse R # redA) b0 b). apply: (compose a) => //. move => H5. move: (H _ _ H5) =>//. move => b0 H1. have:((inverse R # redA) b0 b). apply:(compose a) => //. clear H1 => H1. move: (H _ _ H1); clear H1 H => H. inversion H. clear H4 H5 a0 c0. move: (IHtrans _ H3); clear IHtrans H3. move => H3. inversion H3. clear H6 H7 a0 c0. apply: (compose b2) => //. apply: (tailtransit b1) => //. Qed. (* Reflexive and transitive closure of a relation *) Inductive refltrans {A} (red: Red A) : Red A := | reflex: forall a, refltrans red a a | atleast1: forall a b, trans red a b -> refltrans red a b . (* The transitive closure is equivalent to the composition of the relation with its reflexive-transitive closure *) Lemma trans2refltrans {A} {red: Red A}: trans red -- red # (refltrans red). Proof. rewrite /Equiv/Sub. split => a b H. inversion H. apply:(compose b) => //. apply reflex. apply:(compose b0) => //. apply atleast1 =>//. inversion H. inversion H1. apply:(singl). rewrite H5 in H0 => //. apply:(transit b0) =>//. Qed. (*******************************) (* Strong Normalisation theory *) (* What it means for a predicate to be patriarchal *) Definition patriarchal {A} (red:Red A) (P:A -> Prop): Prop := forall x, (forall y, red x y -> P y) -> P x. (* a is strongly normalising for red *) Definition SN {A:Type} (red:Red A) (a:A): Prop := forall P, patriarchal red P -> P a. (* If all 1-step reducts of a are SN, so is a *) Lemma toSN {A}{red:Red A} {x}: (forall y, red x y -> SN red y) -> SN red x. Proof. rewrite/SN => H P H1. move:(H1); rewrite/patriarchal. apply => y H2. apply H => //. Qed. (* Being SN is a patriarchal predicate *) Lemma SNpatriarchal {A} {red: Red A}: patriarchal red (SN red). Proof. rewrite /patriarchal => M H. rewrite/SN => P H1; apply: (H1); intros. move: (H y H0). apply => //. Qed. (* If M is SN, so are its 1-step reducts *) Lemma SNstable {A} {red: Red A}: forall M, SN red M -> forall N, red M N -> SN red N. Proof. have : (patriarchal red (fun a => forall b, red a b -> SN red b)). move => P /= H. move : (@SNpatriarchal A red) => H1. rewrite /patriarchal in H1 => R HR. apply: H1. apply: H => //. intros. by apply (H _ x). Qed. (* Induction principle: Let P be a predicate such that, for all SN elements a, if the 1-step reducts of a satisfy P then a satisfies P. Then all SN elements satisfy P *) Theorem SNind {A} {red: Red A} {P: A -> Prop} : (forall a, (forall b, red a b -> P b) -> SN red a -> P a) -> (forall a, SN red a -> P a). Proof. move => H3. have: (patriarchal red (fun a => SN red a -> P a)). rewrite /patriarchal => N H H0. apply: H3 =>//. move => R H2. apply: H => //. apply (SNstable N) => //. move => H0 M H1. apply: (H1 (fun a : A => SN red a -> P a)) => //. Qed. (* Being patriarchal for red1 is monotonic in red1 *) Lemma Patriarchalmonotonic {A} {red1 red2: Red A}: red1 <# red2 -> forall P, patriarchal red1 P -> patriarchal red2 P. Proof. rewrite /Sub/patriarchal => H0 P H1 a H2. apply: H1. move => y H1. apply: H2. apply H0 =>//. Qed. (* Being SN for red1 is anti-monotonic in red1 *) Lemma SNmonotonic {A} {red1 red2: Red A}: red1 <# red2 -> forall a, SN red2 a -> SN red1 a. Proof. rewrite/SN. move => H0 a H1 P H2. apply: H1. apply: (Patriarchalmonotonic H0 P H2). Qed. (* Being SN for a relation is the same thing as being SN for its transitive closure *) Lemma SNSNtrans {A} {red: Red A}: forall a, SN red a <-> SN (trans red) a. Proof. split;[| apply: SNmonotonic => //; apply transSub]. have: (forall M, SN red M -> forall N, refltrans red M N -> SN (trans red) N). apply (@SNind _ _ (fun M => forall N, refltrans red M N -> SN (trans red) N)). move => M IH MSN. have:(forall N, trans red M N -> SN (trans red) N). move => N H. move: (proj1 trans2refltrans _ _ H); clear H => H. inversion H. apply:(IH b) => //. move => H. move: (@SNpatriarchal _ (trans red)). rewrite/patriarchal. move => H1. move: (H1 M H); clear H H1 => H N H1. inversion H1. by rewrite <- H2. apply:(SNstable M) => //. intros. apply:(x a) =>//. apply: reflex. Qed. (* Strong Induction principle: Let P be a predicate such that, for all SN elements a, if the n-step reducts of a satisfy P then a satisfies P. Then all SN elements satisfy P. This theorem is stronger than the previous version, since the induction hypothesis can be applied not only to the 1-step reducts, but to all n-step reducts. In the natural numbers, we can assume the IH holds not only for n-1, but for all m Prop} : (forall a, (forall b, trans red a b -> P b) -> SN red a -> P a) -> (forall a, SN red a -> P a). Proof. move => H a H0. move: (proj1(SNSNtrans a)H0). clear H0; move: a. apply SNind. move => a H0 H1. apply H => //. apply SNSNtrans =>//. Qed. (* Strong normalisation by simulation: Assume redA is strongly simulated by redB through R. If a is the image of some element that is SN for redB, then a is SN for redA. *) Theorem SNbySimul {A B} {redA: Red A} {redB: Red B} {R: Rel A B}: StrongSimul redA redB R -> forall a, Image (inverse R) (SN redB) a -> SN redA a. Proof. move => H M H0. inversion H0; clear H0 H3 b. move : a H1 M H2. apply (@SNsind _ _ (fun a => forall M : A, inverse R a M -> SN redA M)). move => N H0 SNN M H1. apply SNpatriarchal => M' H2. rewrite /StrongSimul/Sub in H. have:((inverse R # redA) N M'). apply: (compose M)=>//. move => H3. move:(H _ _ H3); clear H H3 => H. inversion H; clear H5 H6 a c. apply:(H0 b) =>//. Qed.