(***********************************************************) (* This file is distributed under the terms of the *) (* GNU Lesser General Public License version 3 *) (* *) (* Copyright 2009-2010: Damien Pous. *) (* *) (***********************************************************) (** * Untyping theorem for (non-commutative) rings. *) Require Import Relations List ListSet ZArith. Require Import Program Setoid Morphisms. Set Implicit Arguments. Unset Printing Implicit Defensive. Unset Strict Implicit. (** [X] is the set of variables, it has to come with a decidable equality *) Definition X := nat. (** syntax of terms *) Inductive T: Set := | dot: T -> T -> T | pls: T -> T -> T | opp: 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 | opp _ => idtac | var _ => idtac | one => idtac | zer => idtac end. (* inversion tatics *) Ltac inversion' H := inversion H; subst; clear H. (** printing * #*# *) (** notations *) 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" := (opp x): U_scope. Notation "1" := (one): U_scope. Notation "0" := (zer): U_scope. (** * Definition of the normalisation function, by going through polynoms *) Definition monom := list X. Definition polynom := list (Z * monom). Notation lex e f := (match e with Eq => f | _ => e end). Fixpoint monom_compare (m n: monom) := match m,n with | [],[] => Eq | [],_ => Lt | _ ,[] => Gt | x::m,y::n => lex (nat_compare x y) (monom_compare m n) end. Lemma monom_compare_wspec: forall n m, CompSpec eq (fun _ _ => True) n m (monom_compare n m). Proof. induction n; destruct m; simpl; try constructor; auto. case nat_compare_spec; try constructor; auto. intros ->. case IHn; intros; subst; constructor; auto. Qed. (** ** converting polynoms to terms *) Definition readm (m: monom): T := fold_right (fun x q => var x * q) 1 m. Fixpoint copy t p := match p with | xH => t | xO p => copy t p+copy t p | xI p => copy t p+copy t p+t end. Definition readzm zm := let '(z,m) := zm in match z with | Z0 => 0 | Zpos p => copy (readm m) p | Zneg p => - copy (readm m) p end. Definition read (p: polynom): T := fold_right (fun zm q => readzm zm + q) 0 p. (** ** converting terms to polynoms *) Definition poly_one: polynom := [(1%Z,[])]. Definition poly_zer: polynom := []. Definition poly_var i: polynom := [(1%Z,[i])]. Definition poly_opp (p: polynom): polynom := map (fun zm => let '(z,m) := zm in (Zopp z,m)) p. Definition zm z m p: polynom := if Z_eq_dec z 0 then p else (z,m)::p. Fixpoint poly_pls p: polynom -> polynom := match p with | [] => fun q => q | (x,m)::p' => let fix poly_pls_aux q := match q with | [] => p | (y,n)::q' => match monom_compare m n with | Eq => zm (x+y) m (poly_pls p' q') | Lt => (x,m)::poly_pls p' q | Gt => (y,n)::poly_pls_aux q' end end in poly_pls_aux end. Fixpoint insert x m (p: polynom): polynom := match p with | [] => [(x,m)] | (y,n)::p' => match monom_compare m n with | Eq => zm (x+y) m p' | Lt => (x,m)::p | Gt => (y,n)::insert x m p' end end. Definition rdot y n: polynom -> polynom := map (fun xm => let '(x,m) := xm in (Zmult x y,m++n)). Definition ldot x m: polynom -> polynom := map (fun yn => let '(y,n) := yn in (Zmult x y,m++n)). Fixpoint poly_dot (p q: polynom): polynom := match p,q with | [],_ => poly_zer | _,[] => poly_zer | (x,m)::p', (y,n)::q' => poly_pls (poly_pls (insert (x*y) (m++n) (rdot y n p')) (ldot x m q')) (poly_dot p' q') end. Fixpoint eval (t: T): polynom := match t with | x+y => poly_pls (eval x) (eval y) | x*y => poly_dot (eval x) (eval y) | -x => poly_opp (eval x) | 1 => poly_one | 0 => poly_zer | var i => poly_var i end. (** ** final normalisation function *) Definition norm t := read (eval t). (** * Definition of the typed equality judgement *) 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) | t_opp: forall n m u, typed n m u -> typed n m (-u). Hint Constructors typed. (** 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_opp: forall u n m, typed n m u -> equal n m (u+-u) 0 | dot_compat: forall n m p, Proper (equal n m ==> equal m p ==> equal n p) dot | pls_compat: forall n m, Proper (equal n m ==> equal n m ==> equal n m) pls | opp_compat: forall n m, Proper (equal n m ==> equal n m) opp | trans: forall n m, Transitive (equal n m) | sym: forall n m, Symmetric (equal n m). Existing Instance dot_compat. Existing Instance pls_compat. Existing Instance opp_compat. (** sanity requirements *) Lemma equal_refl: forall n m u, typed n m u -> equal n m u u. Proof. induction 1; econstructor; eauto. Qed. Hint Resolve equal_refl. 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. (** we need those lines to circumvent a bug with setoid_rewrite *) Instance equal_per: forall n m, RelationClasses.PER (equal n m). Proof. intros. constructor. apply sym. apply trans. Qed. Let sym' := sym. Hint Extern 1 (ProperProxy (equal _ _) _) => apply equal_refl; solve [eauto]: typeclass_instances. Hint Extern 1 (ProperProxy (flip (equal _ _)) _) => apply equal_refl; solve [eauto]: typeclass_instances. (** derived typed equalities *) Lemma pls_zer: forall u n m, typed n m u -> equal n m (u+0) u. Proof. intros. rewrite pls_comm; auto. apply zer_pls; auto. Qed. Lemma opp_zer: forall n m, equal n m (-0) 0. Proof. intros. rewrite <- zer_pls by auto. apply pls_opp; auto. Qed. Lemma equal_pls: forall w n m u v, equal n m (u+w) (v+w) -> equal n m u v. Proof with auto. intros w n m u v H. destruct (equal_typed H) as [H0 H1]. inversion' H0. inversion' H1. intros. setoid_rewrite <- zer_pls at 1 2... rewrite <- (@pls_opp w)... rewrite <- 2pls_assoc... setoid_rewrite pls_comm at 2 4... rewrite 2pls_assoc... setoid_rewrite pls_comm at 2 4... apply pls_compat... Qed. Lemma opp_pls: forall n m u v, typed n m u -> typed n m v -> equal n m (-(u+v)) ((-u)+(-v)). Proof with auto. intros. apply equal_pls with (u+v)... rewrite pls_comm, pls_opp, pls_assoc... setoid_rewrite pls_comm at 2... rewrite pls_assoc, <-pls_assoc... rewrite pls_opp, zer_pls... rewrite pls_comm, pls_opp... Qed. Lemma opp_invol: forall u n m, typed n m u -> equal n m (--u) u. Proof with auto. intros. rewrite <- zer_pls... rewrite <- (@pls_opp u)... rewrite <- pls_assoc, pls_opp, pls_zer... Qed. Lemma opp_dot_l: forall n m p a b, typed n m a -> typed m p b -> equal n p (-a*b) (-(a*b)). Proof with eauto. intros. apply equal_pls with (a*b). rewrite <- pls_dot... rewrite pls_comm, pls_opp, zer_dot... rewrite pls_comm, pls_opp... Qed. Lemma opp_dot_r: forall n m p a b, typed n m a -> typed m p b -> equal n p (a*-b) (-(a*b)). Proof with eauto. intros. apply equal_pls with (a*b). rewrite <- dot_pls... rewrite pls_comm, pls_opp, dot_zer... rewrite pls_comm, pls_opp... Qed. Lemma opp_dot: forall n m p a b, typed n m a -> typed m p b -> equal n p (-a*-b) (a*b). Proof. intros. rewrite opp_dot_l, <- opp_dot_r, opp_invol; eauto. Qed. (** * (typed) correctness of the normalisation function *) (** ** [norm] preserves types *) Inductive mtyped: I -> I -> monom -> Prop := | mt_nil: forall n, mtyped n n [] | mt_cons: forall n x q, mtyped (t x) n q -> mtyped (s x) n (x::q). Hint Constructors mtyped. Inductive ptyped: I -> I -> polynom -> Prop := | pt_nil: forall n m, ptyped n m [] | pt_cons: forall n m z x q, mtyped n m x -> ptyped n m q -> ptyped n m ((z,x)::q). Hint Constructors ptyped. Lemma copy_typed: forall n m p, typed n m p -> forall z, typed n m (copy p z). Proof. induction z; simpl; auto. Qed. Lemma readm_typed: forall n m p, mtyped n m p -> typed n m (readm p). Proof. induction 1; simpl; eauto. Qed. Lemma readzm_typed: forall n m z x, mtyped n m x -> typed n m (readzm (z,x)). Proof. intros. destruct z; simpl; auto using copy_typed, readm_typed. Qed. Opaque readzm. Lemma read_typed: forall n m p, ptyped n m p -> typed n m (read p). Proof. induction 1; simpl; eauto using readzm_typed. Qed. Lemma opp_ptyped: forall n m u, ptyped n m u -> ptyped n m (poly_opp u). Proof. induction 1; simpl; eauto. Qed. Lemma pls_ptyped: forall n m u, ptyped n m u -> forall v, ptyped n m v -> ptyped n m (poly_pls u v). Proof. induction 1 as [|n m z x h Hx Hh IH1]; simpl; eauto. induction 1 as [|n m z' y k Hy Hk IH2]; simpl; eauto. case monom_compare; eauto. unfold zm. case Z_eq_dec; intros _; eauto. Qed. Lemma insert_ptyped: forall n m z x u, mtyped n m x -> ptyped n m u -> ptyped n m (insert z x u). Proof. intros n m z x u Hx. induction 1 as [|n m y w h Hw Hh IH]; simpl; eauto. case monom_compare; eauto. unfold zm. case Z_eq_dec; intros _; eauto. Qed. Lemma mt_app: forall n m p h k, mtyped n m h -> mtyped m p k -> mtyped n p (h++k). Proof. induction 1; simpl; eauto. Qed. Hint Resolve mt_app. Opaque poly_pls insert. Lemma ldot_ptyped: forall n m p y q r, mtyped n m q -> ptyped m p r -> ptyped n p (ldot y q r). Proof. unfold ldot. induction 2; simpl; eauto. Qed. Lemma rdot_ptyped: forall n m p y q r, mtyped m n q -> ptyped p m r -> ptyped p n (rdot y q r). Proof. unfold rdot. induction 2; simpl; eauto. Qed. Hint Resolve ldot_ptyped rdot_ptyped. Lemma dot_ptyped: forall n m u, ptyped n m u -> forall p v, ptyped m p v -> ptyped n p (poly_dot u v). Proof. induction 1 as [|n m z x h Hx Hh IH]; intros p v Hv; auto. inversion' Hv; auto. simpl. eauto 12 using pls_ptyped, insert_ptyped. Qed. Hint Resolve dot_ptyped pls_ptyped opp_ptyped copy_typed insert_ptyped. Transparent poly_pls insert. Lemma eval_ptyped: forall n m u, typed n m u -> ptyped n m (eval u). Proof. induction 1; simpl; unfold poly_var, poly_one; eauto. Qed. Theorem norm_typed: forall n m u, typed n m u -> typed n m (norm u). Proof. intros. apply read_typed, eval_ptyped. assumption. Qed. (** ** [norm] is correct w.r.t. [equal] *) Coercion read : polynom >-> T. Hint Resolve eval_ptyped read_typed readm_typed readzm_typed. (** lemmas about the [copy] function *) Lemma copy_succ: forall x n m p, typed n m p -> equal n m (copy p (Psucc x)) (p + copy p x). Proof with auto 7. intros. induction x; simpl; auto. rewrite IHx, <- pls_assoc... setoid_rewrite pls_comm at 3... setoid_rewrite pls_assoc at 2... setoid_rewrite pls_comm at 3... Qed. Lemma copy_compat: forall n m a b x, equal n m a b -> equal n m (copy a x) (copy b x). Proof. intros. induction x using Pind. assumption. destruct (equal_typed H). rewrite 2 copy_succ; trivial. apply pls_compat; trivial. Qed. Lemma copy_plus: forall x y n m p, typed n m p -> equal n m (copy p (x+y)) (copy p x + copy p y). Proof. intros x y n m p H. revert y. induction x using Pind; intro y. rewrite <- Pplus_one_succ_l. rewrite copy_succ; auto. rewrite Pplus_succ_permute_l. rewrite copy_succ; auto. rewrite IHx, copy_succ, pls_assoc; auto. Qed. Lemma copy_pred: forall x n m p, typed n m p -> Plt 1 x -> equal n m (copy p (Ppred x)) (copy p x + - p). Proof. intros. case x using Pcase. discriminate. rewrite Ppred_succ. rewrite copy_succ, pls_comm, pls_assoc; auto. setoid_rewrite pls_comm at 2; auto. rewrite pls_opp, zer_pls; auto. Qed. Lemma copy_minus: forall x y n m p, typed n m p -> Plt y x -> equal n m (copy p (x-y)) (copy p x + - copy p y). Proof. intros x y n m p Hp H. induction y using Pind. rewrite <- Ppred_minus. rewrite copy_pred; auto. apply nat_of_P_lt_Lt_compare_morphism in H. rewrite nat_of_P_succ_morphism in H. rewrite Pminus_succ_r. rewrite copy_pred; auto. rewrite IHy. rewrite <- pls_assoc, copy_succ, opp_pls; auto. apply pls_compat; auto using pls_comm. apply nat_of_P_lt_Lt_compare_complement_morphism. omega. apply nat_of_P_lt_Lt_compare_complement_morphism. rewrite nat_of_P_minus_morphism. unfold nat_of_P at 1. simpl. omega. apply nat_of_P_gt_Gt_compare_complement_morphism. omega. Qed. Lemma copy_dot: forall n m p a b x, typed n m a -> typed m p b -> equal n p (copy a x * b) (copy (a*b) x). Proof. intros. induction x using Pind. eauto. rewrite copy_succ, pls_dot; eauto. rewrite IHx, copy_succ; eauto 6. Qed. Lemma dot_copy: forall n m p a b x, typed m n a -> typed p m b -> equal p n (b * copy a x) (copy (b*a) x). Proof. intros. induction x using Pind. eauto. rewrite copy_succ, dot_pls; eauto. rewrite IHx, copy_succ; eauto 6. Qed. Lemma copy_mult: forall n m a x y, typed n m a -> equal n m (copy a (x*y)) (copy (copy a y) x). Proof. intros. induction x using Pind. eauto. rewrite Pmult_Sn_m. rewrite copy_plus, IHx; eauto. rewrite copy_succ; eauto 6. Qed. Lemma readm_app: forall n m p a b, mtyped n m a -> mtyped m p b -> equal n p (readm (a++b)) (readm a * readm b). Proof. induction 1; intros; simpl. rewrite one_dot; auto. rewrite IHmtyped, dot_assoc; eauto 6. Qed. Lemma copy_readm_app: forall n m p a b x y, mtyped n m a -> mtyped m p b -> equal n p (copy (readm (a++b)) (x*y)) (copy (readm a) x * copy (readm b) y). Proof. intros. rewrite copy_mult, copy_dot; eauto. apply copy_compat. rewrite dot_copy; eauto. apply copy_compat. rewrite readm_app; eauto. Qed. (** lemmas about [readzm] *) Transparent readzm. Lemma zm_correct: forall n m z x p, mtyped n m x -> ptyped n m p -> equal n m (zm z x p) (readzm (z,x) + p). Proof. intros; destruct z; simpl; auto 6. unfold zm. case Z_eq_dec; intros _; simpl; auto. rewrite zer_pls; auto. Qed. Lemma readzm_plus: forall x y n m p, mtyped n m p -> equal n m (readzm (x+y,p)%Z) (readzm (x,p) + readzm (y,p)). Proof with auto 7. intros. simpl. destruct x as [|x|x]. destruct y; auto; rewrite zer_pls... destruct y as [|y|y]... simpl. rewrite pls_zer... simpl. apply copy_plus... simpl. case Pcompare_spec; intro Hxy. subst. rewrite pls_opp... rewrite copy_minus, opp_pls... rewrite pls_comm, opp_invol... apply copy_minus; auto. destruct y as [|y|y]. simpl. rewrite pls_zer; auto. simpl. case Pcompare_spec; intro Hxy. subst. rewrite pls_comm, pls_opp... rewrite copy_minus, pls_comm... rewrite copy_minus, opp_pls, opp_invol... simpl. rewrite copy_plus, opp_pls... Qed. Lemma readzm_zer: forall n m p, equal n m (readzm (0%Z,p)) 0. Proof. simpl. auto. Qed. Lemma readzm_neg: forall n m p x, mtyped n m p -> equal n m (readzm (Zopp x,p)) (-readzm (x,p)). Proof. intros. symmetry. destruct x; simpl. apply opp_zer. auto. apply opp_invol; auto. Qed. Lemma readzm_mult: forall n m p a b x y, mtyped n m a -> mtyped m p b -> equal n p (readzm ((x * y)%Z, a++b)) (readzm (x, a) * readzm (y, b)). Proof. intros. symmetry. destruct x; destruct y; simpl; try abstract eauto using zer_dot, dot_zer; symmetry; try rewrite (copy_readm_app (m:=m)); eauto 7; symmetry. apply zer_dot with m; auto. eapply opp_dot_r; eauto. eapply opp_dot_l; eauto. eapply opp_dot; eauto. Qed. (** correctness of [poly_opp] *) Lemma opp_correct: forall n m u, ptyped n m u -> equal n m (poly_opp u) (-u). Proof with auto. induction 1; simpl. symmetry. apply opp_zer. case z; intros; simpl. rewrite 2 zer_pls... rewrite opp_pls... apply pls_compat... rewrite opp_pls, opp_invol... apply pls_compat... Qed. Opaque readzm. (** correctness of [poly_pls] *) Lemma pls_correct: forall n m u, ptyped n m u -> forall v, ptyped n m v -> equal n m (poly_pls u v) (u+v). Proof with auto. induction 1 as [|i j x m h Hm Hh IH1]; simpl; intros v Hv. rewrite zer_pls... induction Hv as [|i j y n k Hn Hk IH2]; simpl. rewrite pls_zer... case monom_compare_wspec. intros ->. rewrite zm_correct by auto. rewrite readzm_plus, IH1... rewrite <- !pls_assoc... apply pls_compat... setoid_rewrite pls_comm at 3... rewrite <- pls_assoc... apply pls_compat... apply pls_comm... intros _; simpl. rewrite IH1, pls_assoc... intros _; simpl. rewrite IH2... rewrite pls_comm, <- pls_assoc... setoid_rewrite pls_comm at 3... Qed. (** correctness of [insert] *) Lemma insert_correct: forall n m x u v, ptyped n m v -> mtyped n m u -> equal n m (insert x u v) (read [(x,u)]+v). Proof with auto. induction v; intros; simpl. rewrite 2 pls_zer... destruct a. inversion' H. case monom_compare_wspec; intros; subst. rewrite zm_correct, readzm_plus... rewrite pls_assoc, pls_zer... rewrite pls_zer... simpl. rewrite IHv... simpl. rewrite pls_zer... rewrite 2 pls_assoc... apply pls_compat... apply pls_comm... Qed. Opaque insert Zmult. (** lemmas about [ldot] and [rdot] *) Lemma ldot_zer: forall n m p a b, ptyped m n b -> mtyped p m a -> equal p n (ldot 0 a b) 0. Proof. unfold ldot. induction 1; intros; simpl; auto. rewrite IHptyped; auto. rewrite pls_zer, readzm_zer; auto. Qed. Lemma ldot_neg: forall x n m p a b, ptyped m n b -> mtyped p m a -> equal p n (ldot (-x) a b) (-ldot x a b). Proof. unfold ldot. intro. induction 1; intros; simpl. rewrite opp_zer; auto. fold (ldot x a q) in *. fold (ldot (-x) a q) in *. rewrite opp_pls; eauto. rewrite <- Zopp_mult_distr_l. rewrite readzm_neg; eauto. apply pls_compat; eauto. Qed. Lemma ldot_pos_correct: forall x n m p a b, ptyped m n b -> mtyped p m a -> equal p n (ldot (Zpos x) a b) (copy (readm a) x * b). Proof. unfold ldot. intro. induction 1; intros; simpl. rewrite dot_zer; eauto. fold (ldot (Zpos x) a q) in *. rewrite IHptyped; auto. rewrite dot_pls, readzm_mult; eauto. apply pls_compat; eauto 6. Qed. Lemma rdot_zer: forall n m p a b, ptyped n m b -> mtyped m p a -> equal n p (rdot 0 a b) 0. Proof. unfold rdot. induction 1; intros; simpl; auto. rewrite Zmult_0_r. rewrite IHptyped; auto. rewrite pls_zer, readzm_zer; auto. Qed. Lemma rdot_neg: forall x n m p a b, ptyped n m b -> mtyped m p a -> equal n p (rdot (-x) a b) (-rdot x a b). Proof. unfold rdot. intro. induction 1; intros; simpl. symmetry. apply opp_zer. fold (rdot x a q) in *. fold (rdot (-x) a q) in *. rewrite opp_pls; eauto. rewrite <- Zopp_mult_distr_r. rewrite readzm_neg; eauto. apply pls_compat; eauto. Qed. Lemma rdot_pos_correct: forall x n m p a b, ptyped n m b -> mtyped m p a -> equal n p (rdot (Zpos x) a b) (b * copy (readm a) x). Proof. unfold rdot. intro. induction 1; intros; simpl. rewrite zer_dot; eauto. fold (rdot (Zpos x) a q) in *. rewrite IHptyped; auto. rewrite pls_dot, readzm_mult; eauto. apply pls_compat; eauto 6. Qed. Transparent Zmult. (** correctness of [poly_dot] *) Lemma dot_correct: forall n m p u, ptyped n m u -> forall v, ptyped m p v -> equal n p (poly_dot u v) (u*v). Proof. induction 1 as [|i j x m h Hm Hh IH1]; simpl; intros v Hv. rewrite zer_dot; eauto. inversion' Hv; simpl. rewrite dot_zer; eauto. rewrite pls_correct; eauto 6. rewrite pls_correct; eauto 6. rewrite insert_correct; eauto. rewrite dot_pls, 2 pls_dot; eauto. rewrite pls_assoc; eauto 8. repeat apply pls_compat; eauto. simpl. rewrite readzm_mult, pls_zer; eauto. Transparent readzm. destruct z; simpl. rewrite dot_zer, rdot_zer; eauto. rewrite rdot_pos_correct; eauto 6. rewrite opp_dot_r, (rdot_neg (Zpos p0)), rdot_pos_correct; eauto 7. destruct x; simpl. rewrite zer_dot, ldot_zer; eauto. rewrite ldot_pos_correct; eauto 6. rewrite opp_dot_l, (ldot_neg (Zpos p0)), ldot_pos_correct; eauto 7. Qed. Transparent insert. (** summing up, we get the correctness of the [norm] function *) Theorem norm_correct: forall n m u, typed n m u -> equal n m (norm u) u. Proof. unfold norm. induction 1; simpl. rewrite pls_zer by eauto. apply dot_one; auto. rewrite pls_comm, zer_pls; eauto. auto. rewrite dot_correct by eauto. eapply dot_compat; eassumption. rewrite pls_correct by auto. apply pls_compat; assumption. rewrite opp_correct by auto. apply opp_compat; assumption. Qed. Lemma normalise: forall n m u v, typed n m u -> typed n m v -> equal n m (norm u) (norm v) -> equal n m u v. Proof. intros n m u v Hu Hv H. rewrite 2 norm_correct in H; assumption. Qed. End types. (** * The normalisation function is "complete" from the untyped point of view *) (** trivial typing environment *) Definition ttt (x: X) := tt. (** [==] is the untyped equality *) Notation "x == y" := (equal ttt ttt tt tt x y) (at level 70, no associativity). (** the following result is admitted since it is standard, a bit tedious, and does not involve types *) Axiom eval_complete: forall u v, u == v -> eval u = eval v. Theorem norm_complete: forall u v, u == v -> norm u = norm v. Proof. intros. unfold norm. f_equal. apply eval_complete. assumption. Qed. (** * Untyping theorem *) Section erase. Variable I: Set. Variables s t: X -> I. Notation typed := (typed s t). Notation equal := (equal s t). (** untyping theorem for rings *) 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. apply normalise; trivial. apply norm_complete in Huv. rewrite Huv. apply equal_refl. apply read_typed, eval_ptyped. assumption. Qed. End erase.