# Untyping theorem for (non-commutative) rings.

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.

notations
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).

## 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.
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).

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).

sanity requirements

Lemma equal_refl: forall n m u, typed n m u -> equal n m u u.

Lemma equal_typed: forall n m u v, equal n m u v -> typed n m u /\ typed n m v.

we need those lines to circumvent a bug with setoid_rewrite

Instance equal_per: forall n m, RelationClasses.PER (equal n m).
Let sym' := sym.

derived typed equalities

Lemma pls_zer: forall u n m, typed n m u -> equal n m (u+0) u.

Lemma opp_zer: forall n m, equal n m (-0) 0.

Lemma equal_pls: forall w n m u v, equal n m (u+w) (v+w) -> equal n m u v.

Lemma opp_pls: forall n m u v, typed n m u -> typed n m v -> equal n m (-(u+v)) ((-u)+(-v)).

Lemma opp_invol: forall u n m, typed n m u -> equal n m (--u) u.

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)).

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)).

Lemma opp_dot: forall n m p a b, typed n m a -> typed m p b -> equal n p (-a*-b) (a*b).

# (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).

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).

Lemma copy_typed: forall n m p, typed n m p -> forall z, typed n m (copy p z).

Lemma readm_typed: forall n m p, mtyped n m p -> typed n m (readm p).

Lemma readzm_typed: forall n m z x, mtyped n m x -> typed n m (readzm (z,x)).

Lemma read_typed: forall n m p, ptyped n m p -> typed n m (read p).

Lemma opp_ptyped: forall n m u, ptyped n m u -> ptyped n m (poly_opp u).

Lemma pls_ptyped: forall n m u, ptyped n m u -> forall v, ptyped n m v -> ptyped n m (poly_pls u v).

Lemma insert_ptyped: forall n m z x u, mtyped n m x -> ptyped n m u -> ptyped n m (insert z x u).

Lemma mt_app: forall n m p h k, mtyped n m h -> mtyped m p k -> mtyped n p (h++k).

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).

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).

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).

Lemma eval_ptyped: forall n m u, typed n m u -> ptyped n m (eval u).

Theorem norm_typed: forall n m u, typed n m u -> typed n m (norm u).

## norm is correct w.r.t. equal

Coercion read : polynom >-> T.

Lemma copy_succ: forall x n m p, typed n m p -> equal n m (copy p (Psucc x)) (p + copy p x).

Lemma copy_compat: forall n m a b x, equal n m a b -> equal n m (copy a x) (copy b x).

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).

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).

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).

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).

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).

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).

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).

Lemma copy_readm_app: forall n m p a b x y, mtyped n m a -> mtyped m p b ->

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).

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)).

Lemma readzm_zer: forall n m p, equal n m (readzm (0%Z,p)) 0.

Lemma readzm_neg: forall n m p x, mtyped n m p -> equal n m (readzm (Zopp x,p)) (-readzm (x,p)).

Lemma readzm_mult: forall n m p a b x y, mtyped n m a -> mtyped m p b ->

correctness of poly_opp

Lemma opp_correct: forall n m u, ptyped n m u ->
equal n m (poly_opp u) (-u).

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).

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).

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.

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).

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).

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.

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).

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).

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).

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.

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.

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.

# 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.

End erase.