(***********************************************************) (* This file is distributed under the terms of the *) (* GNU Lesser General Public License version 3 *) (* *) (* Copyright 2009-2010: Damien Pous. *) (* *) (***********************************************************) (** * Untyping theorems for: - ## monoids##, - ## semirings##, - ## Kleene algebras##, - ## allegories##, - ## Horn theory of monoids##. - ## residuated monoids without unit (direct proof)##. *) (** The corresponding .v file (with proofs) is #here#; see module #mll# for cyclic MLL and residuated monoids (with unit), module #mall# for cyclic MALL (involutive residuated lattices) and residuated lattices (without additive constants), and module #ring# for non-commutative rings. *) Require Import Relations List. Require Import Program. Require Import Setoid Morphisms. Set Implicit Arguments. Unset Printing Implicit Defensive. Unset Strict Implicit. (** [X] is the set of variables, it could be kept abstract *) Definition X := nat. (** syntax of terms, shared by all proofs. unused constructions will be ignored using the typing rules *) Inductive T: Set := | dot: T -> T -> T | pls: T -> T -> T | inf: T -> T -> T | rdv: T -> T -> T | ldv: T -> T -> T | str: T -> T | dag: T -> T | one: T | zer: T | var: X -> T. (* is some term a ``constructed'' one, i.e., not a Coq variable; this is useful to define some tactics below *) Ltac is_constr x := match x with | dot _ _ => idtac | pls _ _ => idtac | inf _ _ => idtac | rdv _ _ => idtac | ldv _ _ => idtac | str _ => idtac | dag _ => idtac | var _ => idtac | one => idtac | zer => idtac | [] => idtac | _::_ => idtac end. (* inversion tatics *) Ltac inversion' H := inversion H; subst; clear H. (** printing * #*# *) (** notations; note that [*] is the product operation, while [#] is the star operation *) Delimit Scope U_scope with U. Open Scope U_scope. Notation "x + y" := (pls x y) (at level 50, left associativity): U_scope. Notation "x * y" := (dot x y) (at level 40, left associativity): U_scope. Notation "x ^ y" := (inf x y) (at level 30, right associativity): U_scope. Notation "x / y" := (rdv y x) (at level 40, left associativity) : U_scope. Notation "y \ x" := (ldv y x) (at level 40, left associativity) : U_scope. Notation "x #" := (str x) (at level 15, left associativity): U_scope. Notation "x `" := (dag x) (at level 15, left associativity): U_scope. Notation "1" := (one): U_scope. Notation "0" := (zer): U_scope. (** trivial typing environment *) Definition ttt (x: X) := tt. (** is some term equal to zero ? *) Definition is_zer u := match u with 0 => true | _ => false end. Lemma Is_zer u : is_zer u = true -> u=0. Proof. destruct u; firstorder discriminate. Qed. (* tactic to automatically do case analyses on instances of the above tests appearing in the goal *) Ltac destruct_tests tac := repeat match goal with | H: is_zer ?u = true |- _ => try rewrite (Is_zer H) in *; clear H | |- context[is_zer ?x] => match x with context[is_zer _] => fail 1 | _ => idtac end; let H := fresh in case_eq (is_zer x); intro H; try rewrite H in *; try discriminate; tac end. (** cleaning function, that normalises terms w.r.t. annihilating laws *) Fixpoint clean u := match u with | u+v => let u := clean u in let v := clean v in if is_zer u then v else if is_zer v then u else u+v | u*v => let u := clean u in let v := clean v in if is_zer u then 0 else if is_zer v then 0 else u*v | u# => let u := clean u in if is_zer u then 1 else u# | u` => let u := clean u in if is_zer u then 0 else u` | _ => u end. (** a term is strict if its normal form is not zero *) Notation strict u := (is_zer (clean u) = false). (** the cleaning function is idempotent *) Lemma clean_idem: forall u, clean (clean u) = clean u. Proof. induction u; simpl; destruct_tests simpl; try congruence. rewrite <- IHu1 in H. discriminate. rewrite <- IHu2 in H0. discriminate. rewrite <- IHu1 in H. discriminate. rewrite <- IHu2 in H0. discriminate. rewrite <- IHu in H. discriminate. rewrite <- IHu in H. discriminate. Qed. (** auxiliary lemmas about strict terms *) Lemma clean_strict: forall u, strict u -> strict (clean u). Proof. intros. rewrite clean_idem. assumption. Qed. Lemma strict_dot: forall u v, strict (u*v) <-> strict u /\ strict v. Proof. intros. simpl. destruct_tests intuition. Qed. Lemma strict_pls: forall u v, strict (u+v) <-> strict u \/ strict v. Proof. intros. simpl. destruct_tests intuition. Qed. (** ** Untyping theorem for monoids ## *) Module Monoid. Section types. (** [I] is the set of pretypes, [s] and [t] give the typing environment (source and target) *) Variable I: Set. Variables s t: X -> I. (** typing judgement *) Inductive typed: I -> I -> T -> Prop := | t_var: forall x, typed (s x) (t x) (var x) | t_one: forall n, typed n n 1 | t_dot: forall n m o u v, typed n m u -> typed m o v -> typed n o (u*v). (** typed equality judgement *) Inductive equal: I -> I -> relation T := | vrefl: forall x, equal (s x) (t x) (var x) (var x) | orefl: forall n, equal n n 1 1 | dot_assoc: forall u v w n m o p, typed n m u -> typed m o v -> typed o p w -> equal n p (u*(v*w)) ((u*v)*w) | one_dot: forall u n m, typed n m u -> equal n m (1*u) u | dot_one: forall u n m, typed n m u -> equal n m (u*1) u | dot_compat: forall n m p, Proper (equal n m ==> equal m p ==> equal n p) dot | trans: forall n m, Transitive (equal n m) | sym: forall n m, Symmetric (equal n m). End types. (** [untyped] means typed in the trivial environment; [==] is the untyped equality *) Notation untyped u := (typed ttt ttt u _ _). Notation "u == v" := (equal ttt ttt tt tt u v) (at level 70, no associativity). Hint Constructors typed. Section erase. Variable I: Set. Variables s t: X -> I. Notation typed := (typed s t). Notation equal := (equal s t). (* tactic to inverse typing derivations *) Ltac inverse_types := repeat match goal with | t: unit |- _ => destruct t | H: untyped _ |- _ => clear H | H: typed _ _ ?x |- _ => is_constr x; inversion' H end. (** injectivity property of type derivations *) Lemma typeinj: forall u n m, typed n m u -> forall m', typed n m' u -> m=m'. Proof. induction 1; intros; inverse_types; trivial. firstorder (subst; auto). Qed. (* tactic to unify pre-types thanks to the above injectivity property *) Ltac injective_types := repeat match goal with | H1: typed ?n _ ?u, H2: typed ?n _ ?u |- _ => generalize (typeinj H1 H2); intro; subst; clear H2 end. (** equal terms have the same types *) Lemma eqtype: forall u v, u == v -> forall n m, typed n m u <-> typed n m v. Proof. induction 1; split; intro; trivial; inverse_types; eauto. apply t_dot with m; firstorder. apply t_dot with m; firstorder. rewrite <- IHequal2, <- IHequal1; trivial. rewrite IHequal1, IHequal2; trivial. firstorder. firstorder. Qed. (** untyping theorem for monoids *) Theorem untype: forall u v, u == v -> forall n m, typed n m u -> typed n m v -> equal n m u v. Proof. induction 1; intros; inverse_types; injective_types; try solve [econstructor; eauto ]. pose proof (proj1 (eqtype H _ _) H6). pose proof (proj1 (eqtype H0 _ _) H9). injective_types. apply dot_compat with m1; firstorder. pose proof (proj1 (eqtype H _ _) H1). pose proof (proj1 (eqtype H0 _ _) H3). apply trans with y; eauto. apply sym. eauto. Qed. End erase. End Monoid. (** ** Untyping theorem for semirings ## *) Module SemiRing. Section types. (** [I] is the set of pretypes, [s] and [t] give the typing environment (source and target) *) Variable I: Set. Variables s t: X -> I. (** typing judgement *) Inductive typed: I -> I -> T -> Prop := | t_var: forall x, typed (s x) (t x) (var x) | t_one: forall n, typed n n 1 | t_zer: forall n m, typed n m 0 | t_dot: forall n m o u v, typed n m u -> typed m o v -> typed n o (u*v) | t_pls: forall n m u v, typed n m u -> typed n m v -> typed n m (u+v). (* inversion of typing derivations *) Ltac inverse_types := repeat match goal with | H: typed _ _ ?x |- _ => is_constr x; inversion' H end. (** injectivity property for types of strict terms *) Lemma typed_inj: forall u, strict u -> forall n m n' m', typed n m u -> typed n' m' u -> (n=n' <-> m=m'). Proof. intros u Hu n m n' m' H; revert n' m' Hu. induction H; intros; inverse_types; try tauto. inversion Hu. rewrite strict_dot in Hu. destruct Hu. apply IHtyped1 in H6; trivial. apply IHtyped2 in H7; tauto. rewrite strict_pls in Hu. firstorder. Qed. (** typed equality judgement *) Inductive equal: I -> I -> relation T := | vrefl: forall x, equal (s x) (t x) (var x) (var x) | orefl: forall n, equal n n 1 1 | zrefl: forall n m, equal n m 0 0 | dot_assoc: forall u v w n m o p, typed n m u -> typed m o v -> typed o p w -> equal n p (u*(v*w)) ((u*v)*w) | one_dot: forall u n m, typed n m u -> equal n m (1*u) u | dot_one: forall u n m, typed n m u -> equal n m (u*1) u | zer_dot: forall u n m o, typed n m u -> equal o m (0*u) 0 | dot_zer: forall u n m o, typed n m u -> equal n o (u*0) 0 | pls_dot: forall u v w n m o, typed n m u -> typed o n v -> typed o n w -> equal o m ((v+w)*u) (v*u+w*u) | dot_pls: forall u v w n m o, typed n m u -> typed m o v -> typed m o w -> equal n o (u*(v+w)) (u*v+u*w) | pls_assoc: forall u v w n m, typed n m u -> typed n m v -> typed n m w -> equal n m (u+(v+w)) ((u+v)+w) | zer_pls: forall u n m, typed n m u -> equal n m (0+u) u | pls_comm: forall u v n m, typed n m u -> typed n m v -> equal n m (u+v) (v+u) | dot_compat: forall n m p u u' v v', equal n m u u' -> equal m p v v' -> equal n p (u*v) (u'*v') | pls_compat: forall n m u u' v v', equal n m u u' -> equal n m v v' -> equal n m (u+v) (u'+v') | trans: forall n m, Transitive (equal n m) | sym: forall n m, Symmetric (equal n m). (** strict typed equality judgement *) Inductive sequal: I -> I -> relation T := | s_vrefl: forall x, sequal (s x) (t x) (var x) (var x) | s_orefl: forall n, sequal n n 1 1 | s_zrefl: forall n m, sequal n m 0 0 | s_dot_assoc: forall u v w n m o p, typed n m u -> typed m o v -> typed o p w -> sequal n p (u*(v*w)) ((u*v)*w) | s_one_dot: forall u n m, typed n m u -> sequal n m (1*u) u | s_dot_one: forall u n m, typed n m u -> sequal n m (u*1) u | s_pls_dot: forall u v w n m o, strict u -> typed n m u -> typed o n v -> typed o n w -> sequal o m ((v+w)*u) (v*u+w*u) | s_dot_pls: forall u v w n m o, strict u -> typed n m u -> typed m o v -> typed m o w -> sequal n o (u*(v+w)) (u*v+u*w) | s_pls_assoc: forall u v w n m, typed n m u -> typed n m v -> typed n m w -> sequal n m (u+(v+w)) ((u+v)+w) | s_pls_comm: forall u v n m, typed n m u -> typed n m v -> sequal n m (u+v) (v+u) | s_dot_compat: forall n m p u u' v v', sequal n m u u' -> sequal m p v v' -> sequal n p (u*v) (u'*v') | s_pls_compat: forall n m u u' v v', sequal n m u u' -> sequal n m v v' -> sequal n m (u+v) (u'+v') | s_trans: forall n m, Transitive (sequal n m) | s_sym: forall n m, Symmetric (sequal n m). (** strict equality is reflexive at each type, it is contained in equality *) Lemma sequal_refl: forall n m u, typed n m u -> sequal n m u u. Proof. induction 1; econstructor; eauto. Qed. Lemma sequal_equal: forall n m u v, sequal n m u v -> equal n m u v. Proof. induction 1; try solve [econstructor; eauto]. apply sym; assumption. Qed. Hint Constructors typed. (** sanity requirement: equality relates well typed terms only *) Lemma equal_typed: forall n m u v, equal n m u v -> typed n m u /\ typed n m v. Proof. induction 1; intuition eauto. Qed. (** the cleaning function preserves types *) Lemma clean_typed: forall n m u, typed n m u -> typed n m (clean u). Proof. induction 1; simpl; eauto. destruct_tests auto. eauto. destruct_tests auto. Qed. Hint Constructors equal. Hint Resolve sequal_equal sequal_refl clean_typed. Definition trans' n m u := @trans n m u. (** the cleaning function returns a equivalent term *) Lemma clean_correct: forall n m u, typed n m u -> equal n m u (clean u). Proof. induction 1; simpl; auto. destruct_tests idtac; eauto using trans'. destruct_tests idtac; eauto using trans'. apply trans with (clean u + 0); eauto. eapply trans; [apply pls_comm|]; eauto. Qed. End types. (** [untyped] means typed in the trivial environment ; [==] is the untyped equality ; [=s=] is the strict untyped equality *) Notation untyped u := (typed ttt ttt tt tt u). Notation "x == y" := (equal ttt ttt tt tt x y) (at level 70, no associativity). Notation "x =s= y" := (sequal ttt ttt tt tt x y) (at level 70, no associativity). Hint Constructors typed sequal equal. Hint Resolve sequal_equal sequal_refl clean_typed. (* inversion of typing derivations *) Ltac inverse_types := repeat match goal with | H: typed _ _ _ _ ?x |- _ => is_constr x; inversion' H end. (* unification of pre-types by the injectivity property (with case analysis) *) Ltac injective_types := repeat match goal with | H0: strict ?u, H1: typed _ _ ?n _ ?u, H2: typed _ _ ?n _ ?u |- _ => pose proof (proj1 (typed_inj H0 H1 H2) (refl_equal _)); subst; clear H2 | H0: strict ?u, H1: typed _ _ _ ?n ?u, H2: typed _ _ _ ?n ?u |- _ => pose proof (proj2 (typed_inj H0 H1 H2) (refl_equal _)); subst; clear H2 end. (* clearing useless hypotheses *) Ltac clean_untyped := repeat match goal with | t: unit |- _ => destruct t end. Section erase. Variable I: Set. Variables s t: X -> I. Notation typed := (typed s t). Notation equal := (equal s t). Notation sequal := (sequal s t). (** strictly equal terms have the same types *) Lemma sequal_same_types: forall u v, u =s= v -> (forall n m, typed n m u <-> typed n m v). Proof. induction 1; split; intro; clean_untyped; trivial; inverse_types; injective_types; eauto; try solve [repeat econstructor; firstorder]. apply t_dot with m; firstorder. apply t_dot with m; firstorder. rewrite <- IHsequal2, <- IHsequal1. trivial. rewrite IHsequal1, IHsequal2. trivial. Qed. (** untyping theorem for strict equalities *) Lemma suntype: forall u v, u =s= v -> forall n m, typed n m u -> typed n m v -> sequal n m u v. Proof. induction 1; intros; clean_untyped; inverse_types; injective_types; try solve [econstructor; eauto ]. pose proof (sequal_same_types H). pose proof (sequal_same_types H0). apply s_dot_compat with m1; firstorder. pose proof (sequal_same_types H). pose proof (sequal_same_types H0). apply s_trans with y; firstorder. apply s_sym. auto. Qed. (** equal terms reduce to zero at the same time *) Lemma clean_zer: forall u v, u == v -> is_zer (clean u) = is_zer (clean v). Proof. induction 1; auto; clean_untyped; simpl; destruct_tests auto. rewrite <- IHequal1 in IHequal2. discriminate. discriminate. Qed. (** factorisation lemma: equality proofs yield strict equality proofs between the normalised terms *) Lemma factorise: forall u v, u == v -> clean u =s= clean v. Proof. induction 1; clean_untyped; simpl; auto; try solve [destruct_tests auto; eauto 7 using clean_strict]. rewrite (clean_zer H), (clean_zer H0). destruct_tests auto; eauto. rewrite (clean_zer H), (clean_zer H0). destruct_tests auto; eauto. eapply s_trans; eassumption. apply s_sym; trivial. Qed. (** untyping theorem for semirings *) Theorem untype: forall u v, u == v -> forall n m, typed n m u -> typed n m v -> equal n m u v. Proof. intros u v Huv n m Hu Hv. eapply trans. apply (clean_correct Hu). apply sym. eapply trans. apply (clean_correct Hv). apply sym. auto using suntype, factorise. Qed. End erase. End SemiRing. (** ** Untyping theorem for Kleene algebras ## *) Module KleeneAlgebra. Section types. (** [I] is the set of pretypes, [s] and [t] give the typing environment (source and target) *) Variable I: Set. Variables s t: X -> I. (** typing judgement *) Inductive typed: I -> I -> T -> Prop := | t_var: forall x, typed (s x) (t x) (var x) | t_one: forall n, typed n n 1 | t_zer: forall n m, typed n m 0 | t_str: forall n u, typed n n u -> typed n n (u#) | t_dot: forall n m o u v, typed n m u -> typed m o v -> typed n o (u*v) | t_pls: forall n m u v, typed n m u -> typed n m v -> typed n m (u+v). (* inversion of typing derivations *) Ltac inverse_types := repeat match goal with | H: typed _ _ ?x |- _ => is_constr x; inversion' H end. (** injectivity property for types of strict terms *) Lemma typed_inj: forall u, strict u -> forall n m n' m', typed n m u -> typed n' m' u -> (n=n' <-> m=m'). Proof. intros u Hu n m n' m' H; revert n' m' Hu. induction H; intros; inverse_types; try tauto. inversion Hu. rewrite strict_dot in Hu. destruct Hu. apply IHtyped1 in H6; trivial. apply IHtyped2 in H7; tauto. rewrite strict_pls in Hu. firstorder. Qed. (** typed equality judgement *) Inductive equal: I -> I -> relation T := | vrefl: forall x, equal (s x) (t x) (var x) (var x) | orefl: forall n, equal n n 1 1 | zrefl: forall n m, equal n m 0 0 | dot_assoc: forall u v w n m o p, typed n m u -> typed m o v -> typed o p w -> equal n p (u*(v*w)) ((u*v)*w) | one_dot: forall u n m, typed n m u -> equal n m (1*u) u | dot_one: forall u n m, typed n m u -> equal n m (u*1) u | zer_dot: forall u n m o, typed n m u -> equal o m (0*u) 0 | dot_zer: forall u n m o, typed n m u -> equal n o (u*0) 0 | pls_dot: forall u v w n m o, typed n m u -> typed o n v -> typed o n w -> equal o m ((v+w)*u) (v*u+w*u) | dot_pls: forall u v w n m o, typed n m u -> typed m o v -> typed m o w -> equal n o (u*(v+w)) (u*v+u*w) | pls_assoc: forall u v w n m, typed n m u -> typed n m v -> typed n m w -> equal n m (u+(v+w)) ((u+v)+w) | zer_pls: forall u n m, typed n m u -> equal n m (0+u) u | pls_comm: forall u v n m, typed n m u -> typed n m v -> equal n m (u+v) (v+u) | pls_idem: forall u n m, typed n m u -> equal n m (u+u) u | str_fold_left: forall u n, typed n n u -> equal n n (1 + u#*u) (u#) | str_ind_left: forall u v n m, typed n n u -> typed n m v -> equal n m (u*v+v) v -> equal n m (u#*v+v) v | str_ind_right: forall u v n m, typed n n u -> typed m n v -> equal m n (v*u+v) v -> equal m n (v*u#+v) v | dot_compat: forall n m p u u' v v', equal n m u u' -> equal m p v v' -> equal n p (u*v) (u'*v') | pls_compat: forall n m u u' v v', equal n m u u' -> equal n m v v' -> equal n m (u+v) (u'+v') | str_compat: forall n u u', equal n n u u' -> equal n n (u#) (u'#) | trans: forall n m, Transitive (equal n m) | sym: forall n m, Symmetric (equal n m). (** strict typed equality judgement *) Inductive sequal: I -> I -> relation T := | s_vrefl: forall x, sequal (s x) (t x) (var x) (var x) | s_orefl: forall n, sequal n n 1 1 | s_zrefl: forall n m, sequal n m 0 0 | s_dot_assoc: forall u v w n m o p, typed n m u -> typed m o v -> typed o p w -> sequal n p (u*(v*w)) ((u*v)*w) | s_one_dot: forall u n m, typed n m u -> sequal n m (1*u) u | s_dot_one: forall u n m, typed n m u -> sequal n m (u*1) u | s_pls_dot: forall u v w n m o, strict u -> typed n m u -> typed o n v -> typed o n w -> sequal o m ((v+w)*u) (v*u+w*u) | s_dot_pls: forall u v w n m o, strict u -> typed n m u -> typed m o v -> typed m o w -> sequal n o (u*(v+w)) (u*v+u*w) | s_pls_assoc: forall u v w n m, typed n m u -> typed n m v -> typed n m w -> sequal n m (u+(v+w)) ((u+v)+w) | s_pls_comm: forall u v n m, typed n m u -> typed n m v -> sequal n m (u+v) (v+u) | s_pls_idem: forall u n m, typed n m u -> sequal n m (u+u) u | s_str_fold_left: forall u n, typed n n u -> sequal n n (1 + u#*u) (u#) | s_str_ind_left: forall u v n m, strict v -> typed n n u -> typed n m v -> sequal n m (u*v+v) v -> sequal n m (u#*v+v) v | s_str_ind_right: forall u v n m, strict v -> typed n n u -> typed m n v -> sequal m n (v*u+v) v -> sequal m n (v*u#+v) v | s_dot_compat: forall n m p u u' v v', sequal n m u u' -> sequal m p v v' -> sequal n p (u*v) (u'*v') | s_pls_compat: forall n m u u' v v', sequal n m u u' -> sequal n m v v' -> sequal n m (u+v) (u'+v') | s_str_compat: forall n u u', sequal n n u u' -> sequal n n (u#) (u'#) | s_trans: forall n m, Transitive (sequal n m) | s_sym: forall n m, Symmetric (sequal n m). Hint Constructors typed equal sequal. (** strict equality is reflexive at each type, it is contained in equality *) Lemma sequal_refl: forall n m u, typed n m u -> sequal n m u u. Proof. induction 1; econstructor; eauto. Qed. Lemma sequal_equal: forall n m u v, sequal n m u v -> equal n m u v. Proof. induction 1; eauto. eapply trans; eauto. apply sym; assumption. Qed. Lemma equal_refl: forall n m u, typed n m u -> equal n m u u. Proof. intros. apply sequal_equal. apply sequal_refl. assumption. Qed. Definition trans' n m u := @trans n m u. (** Kleene star of zero is one *) Lemma str_zer: forall n, equal n n (0#) 1. Proof. intro n. assert (H: equal n n (0#*1+1) 1). eauto 6 using trans'. eapply trans. 2: apply H. eapply trans. apply sym, str_fold_left; eauto. apply sym. eapply trans. apply H. eapply trans. 2: apply pls_compat. 3: apply sym; eauto. 2: apply equal_refl; eauto. eapply trans. apply sym, zer_pls; auto. auto. Qed. Hint Resolve str_zer. (** sanity requirement: equality relates well typed terms only *) Lemma equal_typed: forall n m u v, equal n m u v -> typed n m u /\ typed n m v. Proof. induction 1; intuition eauto. Qed. (** the cleaning function preserves types *) Lemma clean_typed: forall n m u, typed n m u -> typed n m (clean u). Proof. induction 1; simpl; eauto; destruct_tests auto. eauto. Qed. Hint Resolve clean_typed. (** the cleaning function returns an equivalent term *) Lemma clean_correct: forall n m u, typed n m u -> equal n m u (clean u). Proof. induction 1; simpl; auto; destruct_tests idtac; eauto using trans'. apply trans with (clean u + 0); eauto. eapply trans; [apply pls_comm|]; eauto. Qed. End types. (** [untyped] means typed in the trivial environment ; [==] is the untyped equality ; [=s=] is the strict untyped equality *) Notation untyped u := (typed ttt ttt tt tt u). Notation "x == y" := (equal ttt ttt tt tt x y) (at level 70, no associativity). Notation "x =s= y" := (sequal ttt ttt tt tt x y) (at level 70, no associativity). Hint Constructors typed sequal equal. Hint Resolve sequal_refl clean_typed. (* inversion of typing derivations *) Ltac inverse_types := repeat match goal with | H: typed _ _ _ _ ?x |- _ => is_constr x; inversion' H end. (* unification of pre-types by the injectivity property (with case analysis) *) Ltac injective_types := repeat match goal with | H0: strict ?u, H1: typed _ _ ?n _ ?u, H2: typed _ _ ?n _ ?u |- _ => pose proof (proj1 (typed_inj H0 H1 H2) (refl_equal _)); subst; clear H2 | H0: strict ?u, H1: typed _ _ _ ?n ?u, H2: typed _ _ _ ?n ?u |- _ => pose proof (proj2 (typed_inj H0 H1 H2) (refl_equal _)); subst; clear H2 end. (* clearing useless hypotheses *) Ltac clean_untyped := repeat match goal with | t: unit |- _ => destruct t end. Section erase. Variable I: Set. Variables s t: X -> I. Notation typed := (typed s t). Notation equal := (equal s t). Notation sequal := (sequal s t). (** strictly equal terms have the same types *) Lemma sequal_same_types: forall u v, u =s= v -> (forall n m, typed n m u <-> typed n m v). Proof. induction 1; split; intro; clean_untyped; trivial; inverse_types; injective_types; eauto; try solve [repeat econstructor; firstorder]. rewrite <- IHsequal in H3. inverse_types. injective_types; eauto. rewrite <- IHsequal in H3. inverse_types. injective_types; eauto. apply t_dot with m; firstorder. apply t_dot with m; firstorder. rewrite <- IHsequal2, <- IHsequal1. trivial. rewrite IHsequal1, IHsequal2. trivial. Qed. (** untyping theorem for strict equalities *) Lemma suntype: forall u v, u =s= v -> forall n m, typed n m u -> typed n m v -> sequal n m u v. Proof. induction 1; intros; clean_untyped; inverse_types; injective_types; eauto. pose proof (sequal_same_types H). pose proof (sequal_same_types H0). apply s_dot_compat with m; firstorder. pose proof (sequal_same_types H). pose proof (sequal_same_types H0). apply s_trans with y; firstorder. apply s_sym. auto. Qed. (** equal terms reduce to zero at the same time *) Lemma clean_zer: forall u v, u == v -> is_zer (clean u) = is_zer (clean v). Proof. induction 1; auto; clean_untyped; simpl; destruct_tests auto. rewrite <- IHequal1 in IHequal2. discriminate. discriminate. Qed. (** factorisation lemma: equality proofs yield strict equality proofs between the normalised terms *) Lemma factorise: forall u v, u == v -> clean u =s= clean v. Proof. induction 1; clean_untyped; simpl; auto. destruct_tests auto; eauto using clean_strict. destruct_tests auto; eauto using clean_strict. destruct_tests auto; eauto using clean_strict. destruct_tests auto; eauto using clean_strict. destruct_tests auto; eauto using clean_strict. destruct_tests auto; eauto 7 using clean_strict. destruct_tests auto; eauto 7 using clean_strict. destruct_tests auto; eauto using clean_strict. destruct_tests auto; eauto using clean_strict. destruct_tests auto; eauto using clean_strict. destruct_tests auto; eauto using clean_strict. simpl in *. destruct_tests auto. simpl in *. eapply s_trans. apply s_pls_compat. apply s_one_dot; eauto. eauto. eauto. apply s_str_ind_left; eauto using clean_strict. simpl in *. destruct_tests auto. simpl in *. eapply s_trans. apply s_pls_compat. apply s_dot_one; eauto. eauto. eauto. apply s_str_ind_right; eauto using clean_strict. rewrite (clean_zer H), (clean_zer H0). destruct_tests auto; eauto. rewrite (clean_zer H), (clean_zer H0). destruct_tests auto; eauto. rewrite (clean_zer H). destruct_tests auto; eauto. eapply s_trans; eassumption. apply s_sym; trivial. Qed. (** untyping theorem for Kleene algebras *) Theorem untype: forall u v, u == v -> forall n m, typed n m u -> typed n m v -> equal n m u v. Proof. intros u v Huv n m Hu Hv. eapply trans. apply (clean_correct Hu). apply sym. eapply trans. apply (clean_correct Hv). apply sym. auto using suntype, factorise, sequal_equal. Qed. End erase. End KleeneAlgebra. (** ** Untyping theorem for allegories ## *) Module Allegory. Section types. (** [I] is the set of pretypes, [s] and [t] give the typing environment (source and target) *) Variable I: Set. Variables s t: X -> I. (** typing judgement *) Inductive typed: I -> I -> T -> Prop := | t_var: forall x, typed (s x) (t x) (var x) | t_one: forall n, typed n n 1 | t_dag: forall n m u, typed n m u -> typed m n (u`) | t_dot: forall n m q u v, typed n m u -> typed m q v -> typed n q (u*v) | t_inf: forall n m u v, typed n m u -> typed n m v -> typed n m (u^v). (* inversion of typing derivations *) Ltac inverse_types := repeat match goal with | H: typed _ _ ?x |- _ => is_constr x; inversion' H end. (** injectivity property of typing derivations *) Lemma typed_inj: forall u n m n' m', typed n m u -> typed n' m' u -> (n=n' <-> m=m'). Proof. intros u n m n' m' H; revert n' m'. induction H; intros; inverse_types; try solve [firstorder]. rewrite IHtyped1; eauto. Qed. (** typed equality judgement *) Inductive equal: I -> I -> relation T := | vrefl: forall x, equal (s x) (t x) (var x) (var x) | orefl: forall n, equal n n 1 1 | dot_assoc: forall u v w n m q p, typed n m u -> typed m q v -> typed q p w -> equal n p (u*(v*w)) ((u*v)*w) | one_dot: forall u n m, typed n m u -> equal n m (1*u) u | dot_one: forall u n m, typed n m u -> equal n m (u*1) u | inf_assoc: forall u v w n m, typed n m u -> typed n m v -> typed n m w -> equal n m (u^(v^w)) ((u^v)^w) | inf_comm: forall u v n m, typed n m u -> typed n m v -> equal n m (u^v) (v^u) | dag_invol: forall u n m, typed n m u -> equal n m (u``) u | dag_dot: forall u v n m p, typed n m u -> typed m p v -> equal p n ((u*v)`) (v`*u`) | dag_inf: forall u v n m, typed n m u -> typed n m v -> equal m n ((u^v)`) (u`^v`) | modular_law: forall u v w n m p, typed n m u -> typed m p v -> typed n p w -> equal n p ((u*v) ^ w) ((u*(v^(u`*w))) ^ (u*v) ^ w) | dag_compat: forall n m u u', equal n m u u' -> equal m n (u`) (u'`) | dot_compat: forall n m p u u' v v', equal n m u u' -> equal m p v v' -> equal n p (u*v) (u'*v') | inf_compat: forall n m u u' v v', equal n m u u' -> equal n m v v' -> equal n m (u^v) (u'^v') | trans: forall n m, Transitive (equal n m) | sym: forall n m, Symmetric (equal n m). (** strict equality is reflexive at each type, and relates well-typed terms only *) Lemma equal_refl: forall n m u, typed n m u -> equal n m u u. Proof. induction 1; econstructor; eauto. Qed. Hint Constructors typed. Lemma equal_typed: forall n m u v, equal n m u v -> typed n m u /\ typed n m v. Proof. induction 1; intuition eauto 8. Qed. End types. (** [untyped] means typed in the trivial environment, [==] is the untyped equality *) Notation untyped u := (typed ttt ttt tt tt u). Notation "x == y" := (equal ttt ttt tt tt x y) (at level 70, no associativity). Hint Constructors typed equal. Hint Resolve equal_refl. (* inversion of typing derivations *) Ltac inverse_types := repeat match goal with | H: typed _ _ _ _ ?x |- _ => is_constr x; inversion' H end. (* unification of pre-types by the injectivity property (with case analysis) *) Ltac injective_types := repeat match goal with | H1: typed _ _ ?n _ ?u, H2: typed _ _ ?n _ ?u |- _ => pose proof (proj1 (typed_inj H1 H2) (refl_equal _)); subst; clear H2 | H1: typed _ _ _ ?n ?u, H2: typed _ _ _ ?n ?u |- _ => pose proof (proj2 (typed_inj H1 H2) (refl_equal _)); subst; clear H2 end. (* clearing useless hypotheses *) Ltac clean_untyped := repeat match goal with | t: unit |- _ => destruct t end. Section erase. Variable I: Set. Variables s t: X -> I. Notation typed := (typed s t). Notation equal := (equal s t). (** equal terms have the same types *) Lemma equal_same_types: forall u v, u == v -> (forall n m, typed n m u <-> typed n m v). Proof. induction 1; split; intro; clean_untyped; trivial; inverse_types; injective_types; eauto; try solve [repeat econstructor; firstorder]. eauto 8. apply t_dot with m; firstorder. apply t_dot with m; firstorder. rewrite <- IHequal2, <- IHequal1. trivial. rewrite IHequal1, IHequal2. trivial. Qed. (** untyping theorem for allegories *) Theorem untype: forall u v, u == v -> forall n m, typed n m u -> typed n m v -> equal n m u v. Proof. induction 1; intros; clean_untyped; inverse_types; injective_types; try solve [econstructor; eauto ]. pose proof (equal_same_types H). pose proof (equal_same_types H0). apply dot_compat with m1; firstorder. pose proof (equal_same_types H). pose proof (equal_same_types H0). apply trans with y; firstorder. apply sym. auto. Qed. End erase. End Allegory. (** ** Untyping theorem for the Horn theory of monoids ## *) Module HornMonoid. Section types. (** [I] is the set of pretypes, [s] and [t] give the typing environment (source and target) *) Variable I: Set. Variables s t: X -> I. (** untyped proof assumptions (Horn hypotheses) *) Variable h: I -> I -> relation T. (** typing judgement *) Inductive typed: I -> I -> T -> Prop := | t_var: forall x, typed (s x) (t x) (var x) | t_one: forall n, typed n n 1 | t_dot: forall n m o u v, typed n m u -> typed m o v -> typed n o (u*v). (** typed equality judgement *) Inductive equal: I -> I -> relation T := | vrefl: forall x, equal (s x) (t x) (var x) (var x) | orefl: forall n, equal n n 1 1 | dot_assoc: forall u v w n m o p, typed n m u -> typed m o v -> typed o p w -> equal n p (u*(v*w)) ((u*v)*w) | one_dot: forall u n m, typed n m u -> equal n m (1*u) u | dot_one: forall u n m, typed n m u -> equal n m (u*1) u | dot_compat: forall n m p, Proper (equal n m ==> equal m p ==> equal n p) dot | hyp: forall u v n m, h n m u v -> equal n m u v | trans: forall n m, Transitive (equal n m) | sym: forall n m, Symmetric (equal n m). End types. (** [untyped] means typed in the trivial environment; [==] is the untyped equality *) Notation untyped u := (typed ttt ttt u _ _). Hint Constructors typed. Section erase. Variable I: Set. Variables s t: X -> I. Variable h: I -> I -> relation T. Definition tth (_ _: unit) := fun u v => exists n m , h n m u v. Notation "u == v" := (equal ttt ttt tth tt tt u v) (at level 70, no associativity). Notation typed := (typed s t). Notation equal := (equal s t h). (** typing requirement about the Horn context *) Hypothesis h_typed: forall n m u v, h n m u v -> typed n m u /\ typed n m v. Hypothesis h_utyped: forall n m u v, h n m u v -> forall p q, typed p q u \/ typed p q v -> p=n /\ q=m. Lemma h_utyped2: forall n m u v, h n m u v -> forall p q, typed p q u -> typed p q v -> p=n /\ q=m. Proof. intros. eauto. Qed. Lemma h_eqtyped: forall n m u v, h n m u v -> forall p q, typed p q u <-> typed p q v. Proof. intros. destruct (h_typed H) as [Hu Hv]. assert (H' := h_utyped H). specialize (H' p q). firstorder subst; trivial. Qed. (* h_typed -> (h_typed <-> h_utyped2 /\ h_eqtyped) *) Lemma h_utyped': forall n m u v, h n m u v -> forall p q, typed p q u \/ typed p q v -> p=n /\ q=m. Proof. clear h_utyped. intros n m u v H p q [H'|H']; eapply h_utyped2; eauto; pose proof (h_eqtyped H p q); tauto. Qed. (* tactic to inverse typing derivations *) Ltac inverse_types := repeat match goal with | t: unit |- _ => destruct t | H: untyped _ |- _ => clear H | H: typed _ _ ?x |- _ => is_constr x; inversion' H end. (** injectivity property of type derivations *) Lemma typeinj: forall u n m, typed n m u -> forall m', typed n m' u -> m=m'. Proof. induction 1; intros; inverse_types; trivial. firstorder (subst; auto). Qed. Lemma typeinj': forall u n m, typed n m u -> forall n' m', typed n' m' u -> n=n' /\ m=m' \/ n=m /\ n'=m'. Proof. induction 1; intros; inverse_types; auto. apply IHtyped1 in H6. apply IHtyped2 in H7. clear - H6 H7. intuition subst; auto. Qed. (* tactic to unify pre-types thanks to the above injectivity property *) Ltac injective_types := repeat match goal with | H1: typed ?n _ ?u, H2: typed ?n _ ?u |- _ => generalize (typeinj H1 H2); intro; subst; clear H2 end. (** equal terms have the same types *) Lemma eqtype: forall u v, u == v -> forall n m, typed n m u <-> typed n m v. Proof. induction 1; split; intro; trivial; inverse_types; eauto. apply t_dot with m; firstorder. apply t_dot with m; firstorder. destruct H as (?&?&H). eapply h_eqtyped in H. firstorder eauto. destruct H as (?&?&H). eapply h_eqtyped in H. firstorder eauto. rewrite <- IHequal2, <- IHequal1; trivial. rewrite IHequal1, IHequal2; trivial. firstorder. firstorder. Qed. (** untyping theorem for monoids *) Theorem untype: forall u v, u == v -> forall n m, typed n m u -> typed n m v -> equal n m u v. Proof. induction 1; intros; inverse_types; injective_types; try solve [econstructor; eauto ]. pose proof (proj1 (eqtype H _ _) H6). pose proof (proj1 (eqtype H0 _ _) H9). injective_types. apply dot_compat with m1; firstorder. destruct H as (n&m&H). destruct (h_utyped2 H H0 H1); subst. apply hyp; assumption. pose proof (proj1 (eqtype H _ _) H1). pose proof (proj1 (eqtype H0 _ _) H3). apply trans with y; eauto. apply sym. eauto. Qed. End erase. End HornMonoid. (** ** Untyping theorem for residuated monoids without units : direct proof ##, see module #mll# for the proof with units, through cyclic MLL *) Module UnitFreeResMonoid. Section types. (** [I] is the set of pretypes, [s] and [t] give the typing environment (source and target) *) Variable I: Set. Variables s t: X -> I. (** typing judgement *) Inductive typed: I -> I -> T -> Prop := | t_var: forall x, typed (s x) (t x) (var x) | t_rdv: forall n m o u v, typed n o u -> typed m o v -> typed n m (u/v) | t_ldv: forall n m o u v, typed n o u -> typed n m v -> typed m o (v\u) | t_dot: forall n m o u v, typed n m u -> typed m o v -> typed n o (u*v). (** typing judgement for lists of terms *) Inductive ltyped: I -> I -> list T -> Prop := | t_nil: forall n, ltyped n n [] | t_cons: forall n m p l u, typed n m u -> ltyped m p l -> ltyped n p (u::l). (** weak typing judgement for lists: each element has to be typeable *) Inductive lwtyped: list T -> Prop := | wt_nil: lwtyped [] | wt_cons: forall n m l u, typed n m u -> lwtyped l -> lwtyped (u::l). Hint Constructors typed ltyped lwtyped. (** typing a concatenation *) Lemma t_app: forall l l' n m p, ltyped n m l -> ltyped m p l' -> ltyped n p (l++l'). Proof. intros. induction H; simpl; eauto. Qed. Hint Resolve t_app. (** inversion lemma for typing judgements about concatenated lists *) Lemma t_app_inv: forall l l' n p, ltyped n p (l++l') -> exists2 m, ltyped n m l & ltyped m p l'. Proof. induction l; intros. eauto. inversion_clear H. destruct (IHl _ _ _ H1). eauto. Qed. (** any typed list is weakly typed *) Lemma lt_lwt: forall l n m, ltyped n m l -> lwtyped l. Proof. induction 1; eauto. Qed. (** weakly typing a concatenation *) Lemma wt_app: forall l l', lwtyped l -> lwtyped l' -> lwtyped (l++l'). Proof. intros. induction H; simpl; eauto. Qed. (** inversion lemma for weak typing judgements about concatenated lists *) Lemma wt_app_inv: forall l l', lwtyped (l++l') -> lwtyped l /\ lwtyped l'. Proof. induction l; intros l' H; simpl; auto. inversion_clear H. destruct (IHl _ H1). eauto. Qed. (* inversion of typing derivations *) Ltac inverse_types := repeat match goal with | H: typed _ _ ?x |- _ => is_constr x; inversion' H | H: ltyped _ _ ?x |- _ => is_constr x; inversion' H | H: ltyped _ _ (_++_) |- _ => destruct (t_app_inv H); clear H end. (** (strong) injectivity property of typing judgements *) Lemma typed_inj: forall u n m, typed n m u -> forall n' m', typed n' m' u -> n=n' /\ m=m'. Proof. induction 1; intros; inverse_types; firstorder. Qed. (* unification of pre-types thanks to the previous property *) Ltac injective_types := repeat match goal with | H1: typed _ _ ?u, H2: typed _ _ ?u |- _ => destruct (typed_inj H1 H2); repeat subst; clear H2 end. (** typed sequent proof system *) Inductive leq: I -> I -> list T -> T -> Prop := | leq_var: forall i, leq (s i) (t i) [var i] (var i) | dot_intro: forall l l' u u' n m p, leq n m l u -> leq m p l' u' -> leq n p (l++l') (u*u') | dot_elim: forall l v w l' u n m, leq n m (l++v::w::l') u -> leq n m (l++(v*w)::l') u | rdv_intro: forall u v l n m p, typed m p v -> leq n p (l++[v]) u -> leq n m l (u/v) | rdv_elim: forall l k v w l' u n m p o i, typed i m w -> leq n m k v -> leq p o (l++w::l') u -> leq p o (l++(w/v)::k++l') u | ldv_intro: forall u v l n m p, typed p m v -> leq p n (v::l) u -> leq m n l (v\u) | ldv_elim: forall l k v w l' u n m p o i, typed m i w -> leq m n k v -> leq o p (l++w::l') u -> leq o p (l++k++(v\w)::l') u . Hint Constructors leq. (** sanity checks: derivable sequents are correctly typed; the proof system is "reflexive" *) Lemma leq_typed: forall l u n m, leq n m l u -> ltyped n m l /\ typed n m u. Proof. induction 1; intuition (inverse_types; injective_types; eauto). Qed. Lemma leq_refl: forall u n m, typed n m u -> leq n m [u] u. Proof. induction 1; eauto. econstructor. eassumption. eapply (rdv_elim (l:=[]) (k:=v::[]) (l':=[])); eauto. econstructor. eassumption. refine (ldv_elim (l:=[]) (k:=v::[]) (l':=[]) _ _ _); eauto. apply (dot_elim (l:=[])). eapply (dot_intro (l:=u::[]) (l':=v::[])); eauto. Qed. End types. (** [untyped] means typed in the trivial environment ; [<==] is untyped derivability ; *) Notation untyped u := (typed ttt ttt u _ _). Notation "x <== y" := (leq ttt ttt tt tt x y) (at level 70, no associativity). Hint Constructors leq typed ltyped lwtyped. Hint Resolve t_app wt_app lt_lwt. Section erase. Variable I: Set. Variables s t: X -> I. Notation lwtyped := (lwtyped s t). Notation ltyped := (ltyped s t). Notation typed := (typed s t). Notation leq := (leq s t). (* inversion of typing derivations *) Ltac inverse_types := repeat match goal with | H: typed _ _ ?x |- _ => is_constr x; inversion' H | H: ltyped _ _ ?x |- _ => is_constr x; inversion' H | H: ltyped _ _ (_++_) |- _ => destruct (t_app_inv H); clear H | H: lwtyped ?x |- _ => is_constr x; inversion' H | H: lwtyped (_++_) |- _ => destruct (wt_app_inv H); clear H end. (* unification of pre-types by the injectivity property *) Ltac injective_types := repeat match goal with | H1: typed _ _ ?u, H2: typed _ _ ?u |- _ => destruct (typed_inj H1 H2); repeat subst; clear H2 end. (* clearing useless hypotheses *) Ltac clean_untyped := repeat match goal with | t: unit |- _ => destruct t | H: untyped _ |- _ => clear H end. (** key lemma *) Lemma untype_aux: forall l u, l <== u -> lwtyped l -> forall n m, typed n m u -> leq n m l u. Proof. induction 1; intros; clean_untyped; inverse_types; injective_types; eauto 6. Qed. (** untyping theorem for residuated monoids without units *) Theorem untype: forall l u, l <==u -> forall n m, ltyped n m l -> typed n m u -> leq n m l u. Proof. intros. eauto using untype_aux. Qed. End erase. End UnitFreeResMonoid.