Set Implicit Arguments. Unset Strict Implicit. Require Import Arith. Require Export notation. Module Algebra_notation. Export Notation. Definition Plus := (p_(l_(u_(s_(DOT 2))))). Definition casePlus a (b : notn) op := match op return (atof op) with (p_(l_(u_(s_(DOT 2))))) => a | z => (b z) end. Definition Times := (t_(i_(m_(s_(DOT 2))))). Definition caseTimes a (b : notn) op := match op return (atof op) with (t_(i_(m_(s_(DOT 2))))) => a | z => (b z) end. Definition Mult := (m_(u_(l_(t_(DOT 2))))). Definition caseMult a (b : notn) op := match op return (atof op) with (m_(u_(l_(t_(DOT 2))))) => a | z => (b z) end. Definition Scalars := (s_(c_(a_(l_(DOT 0))))). Definition caseScalars a (b : notn) op := match op return (atof op) with (s_(c_(a_(l_(DOT 0))))) => a | z => (b z) end. Definition Index := (i_(n_(d_(x_(DOT 0))))). Definition caseIndex a (b : notn) op := match op return (atof op) with (i_(n_(d_(x_(DOT 0))))) => a | z => (b z) end. Definition Degree := (d_(e_(g_(r_(DOT 2))))). Definition caseDegree a (b : notn) op := match op return (atof op) with (d_(e_(g_(r_(DOT 2))))) => a | z => (b z) end. Definition plus' (x a b : E) := extra x Plus a b. Definition times' (x a b : E) := extra x Times a b. Definition mult' (x a b : E) := extra x Mult a b. Definition scalars (x : E) := extra x Scalars. Definition index (x : E) := extra x Index. Definition degree' (x a b : E) := extra x Degree a b. Definition times (a x y : E) := mask (A (inc x (U a)) (inc y (U a))) (times' a x y). Definition plus (a x y : E) := mask (A (inc x (U a)) (inc y (U a))) (plus' a x y). Definition mult (a x y : E) := mask (A (inc x (U (scalars a))) (inc y (U a))) (mult' a x y). Definition degree (a i x : E) := A (inc i (U (index a))) (A (inc x (U a)) (nonempty (degree' a i x))). Lemma times_prime : forall a x y : E, inc x (U a) -> inc y (U a) -> times a x y = times' a x y. ir. uf times. ap mask_in. ee; am. Qed. Lemma plus_prime : forall a x y : E, inc x (U a) -> inc y (U a) -> plus a x y = plus' a x y. ir. uf plus. ap mask_in. ee; am. Qed. Lemma mult_prime : forall a x y : E, inc x (U (scalars a)) -> inc y (U a) -> mult a x y = mult' a x y. ir. uf mult. ap mask_in. ee; am. Qed. Lemma degree_prime : forall a i x : E, inc i (U (index a)) -> inc x (U a) -> degree a i x = nonempty (degree' a i x). ir. uf degree. ap iff_eq; ir; ee; am. Qed. Lemma times_eq : forall a b : E, U a = U b -> (forall x y : E, inc x (U a) -> inc y (U a) -> times a x y = times b x y) -> times a = times b. ir. ap arrow_extensionality; intro x. ap arrow_extensionality; intro y. apply by_cases with (inc x (U a)). ir. apply by_cases with (inc y (U a)). ir. ap H0; am. ir. uf times. rw mask_out. rw mask_out. tv. uf not; ir. ap H2. ee. rw H; am. uf not; ir. ap H2. ee; am. ir. uf times. rw mask_out. rw mask_out. tv. uf not; ir. ap H1. rw H; ee; am. uf not; ir. ap H1. ee; am. Qed. Lemma plus_eq : forall a b : E, U a = U b -> (forall x y : E, inc x (U a) -> inc y (U a) -> plus a x y = plus b x y) -> plus a = plus b. ir. ap arrow_extensionality; intro x. ap arrow_extensionality; intro y. apply by_cases with (inc x (U a)). ir. apply by_cases with (inc y (U a)). ir. ap H0; am. ir. uf plus. rw mask_out. rw mask_out. tv. uf not; ir. ap H2. ee. rw H; am. uf not; ir. ap H2. ee; am. ir. uf plus. rw mask_out. rw mask_out. tv. uf not; ir. ap H1. rw H; ee; am. uf not; ir. ap H1. ee; am. Qed. Lemma mult_eq : forall a b : E, U a = U b -> scalars a = scalars b -> (forall x y : E, inc x (U (scalars a)) -> inc y (U a) -> mult a x y = mult b x y) -> mult a = mult b. ir. ap arrow_extensionality; intro x. ap arrow_extensionality; intro y. apply by_cases with (inc x (U (scalars a))). ir. apply by_cases with (inc y (U a)). ir. ap H1; am. ir. uf mult. rw mask_out. rw mask_out; tv. uf not; ir. ap H3. rw H; ee; am. uf not; ir. ap H3. ee; am. ir. uf mult. rw mask_out. rw mask_out; tv. uf not; ir. ap H2; rw H0; ee; am. uf not; ir. ap H2; ee; am. Qed. Lemma degree_eq : forall a b : E, U a = U b -> index a = index b -> (forall i x : E, inc i (U (index a)) -> inc x (U a) -> degree a i x = degree b i x) -> degree a = degree b. ir. ap arrow_extensionality; intro i. ap arrow_extensionality; intro x. apply by_cases with (inc i (U (index a))). ir. apply by_cases with (inc x (U a)). ir. ap H1; am. ir. ap iff_eq. ir. uh H4; ee. assert False. ap H3. am. elim H7. ir. assert False. uh H4; ee. ap H3. rw H. am. elim H5. ir. ap iff_eq; ir. assert False. ap H2. uh H3; ee; am. elim H4. assert False. ap H2. rw H0. uh H3; ee; am. elim H4. Qed. Lemma degree_addl : forall a i x : E, degree a i x = A (inc i (U (index a))) (A (inc x (U a)) (degree a i x)). ir. ap iff_eq; ir. dj. uh H; ee; am. uh H; ee; am. am. ee; am. Qed. Section def. Variables x v_scalars v_index : E. Variables v_plus v_times v_mult : E2. Variable v_degree : E2P. Definition create_obj op := caseUnderlying x ( casePlus v_plus ( caseScalars v_scalars ( caseIndex v_index ( caseTimes v_times ( caseMult v_mult ( caseDegree v_degree da)))))) op. Definition create_ens := createN create_obj. Lemma related_obj : forall a : E, inc a x -> related create_obj a. ir. sub_relate (u_(n_(d_(r_(DOT 0))))). am. Qed. Lemma scalars_related_obj : forall a : E, inc a (U v_scalars) -> related create_obj a. ir. cp (region_preserves create_obj Scalars). assert (related create_obj (U v_scalars)). ap related_U. am. uh H1. uhg. ap (region_preserves_sub H1). am. Qed. Lemma index_related_obj : forall a : E, inc a (U v_index) -> related create_obj a. ir. cp (region_preserves create_obj Index). assert (related create_obj (U v_index)). ap related_U. am. uh H1. uhg. ap (region_preserves_sub H1). am. Qed. Lemma U_rw : U create_ens = x. ir; uf U; uf create_ens. notatac1; am. Qed. Lemma scalars_rw : scalars create_ens = v_scalars. ir; uf scalars; uf create_ens. notatac1; am. Qed. Lemma index_rw : index create_ens = v_index. ir; uf index; uf create_ens. notatac1; am. Qed. Lemma times_rw : forall a b : E, inc a x -> inc b x -> times create_ens a b = v_times a b. ir. rw times_prime. uf times'; uf create_ens. notatac1; ap related_obj; am. rw U_rw. am. rw U_rw. am. Qed. Lemma plus_rw : forall a b : E, inc a x -> inc b x -> plus create_ens a b = v_plus a b. ir. rw plus_prime. uf plus'; uf create_ens. notatac1; ap related_obj; am. rw U_rw. am. rw U_rw. am. Qed. Lemma mult_rw : forall a b : E, inc a (U v_scalars) -> inc b x -> mult create_ens a b = v_mult a b. ir. rw mult_prime. uf mult'; uf create_ens. notatac1. ap scalars_related_obj. am. ap related_obj. am. rw scalars_rw. am. rw U_rw. am. Qed. Lemma degree_rw : forall i a : E, inc i (U v_index) -> inc a x -> degree create_ens i a = v_degree i a. ir. rw degree_prime. uf degree'; uf create_ens. assert (extra (createN create_obj) Degree i a = v_degree i a). notatac1. ap index_related_obj. am. ap related_obj. am. rw H1. ap iff_eq; ir. nin H2. exact (B H2). sh (R H2). ap R_inc. rw index_rw. am. rw U_rw; am. Qed. End def. Definition like (a : E) := create_ens (U a) (scalars a) (index a) (plus a) ( times a) (mult a) (degree a) = a. Definition same (a b : E) := A (U a = U b) (A (scalars a = scalars b) (A (index a = index b) (A (plus a = plus b) (A (times a = times b) (A (mult a = mult b) (degree a = degree b)))))). Lemma show_same : forall a b : E, U a = U b -> scalars a = scalars b -> index a = index b -> (forall x y : E, inc x (U a) -> inc y (U a) -> plus a x y = plus b x y) -> (forall x y : E, inc x (U a) -> inc y (U a) -> times a x y = times b x y) -> (forall x y : E, inc x (U (scalars a)) -> inc y (U a) -> mult a x y = mult b x y) -> (forall i x : E, inc i (U (index a)) -> inc x (U a) -> degree a i x = degree b i x) -> same a b. ir. uhg; dj. am. am. am. ap plus_eq; am. ap times_eq; am. ap mult_eq; am. ap degree_eq; am. Qed. Lemma like_same_eq : forall a b : E, like a -> like b -> same a b -> a = b. ir. uh H. uh H0. wr H. wr H0. uh H1; ee. rw H1. rw H2. rw H3. rw H4. rw H5. rw H6. rw H7. tv. Qed. Lemma create_same : forall a : E, same a (create_ens (U a) (scalars a) (index a) (plus a) ( times a) (mult a) (degree a)). ir. ap show_same; ir. rw U_rw. tv. rw scalars_rw; tv. rw index_rw; tv. rw plus_rw. tv. am. am. rw times_rw. tv. am. am. rw mult_rw. tv. am. am. rw degree_rw. tv. am. am. Qed. Lemma create_like : forall a : E, like (create_ens (U a) (scalars a) (index a) (plus a) ( times a) (mult a) (degree a)). ir. set (K := create_ens (U a) (scalars a) (index a) (plus a) ( times a) (mult a) (degree a)) in *. uhg. assert (same a K). uf K; ap create_same. uh H; ee. wr H; wr H0; wr H1; wr H2; wr H3; wr H4; wr H5. tv. Qed. End Algebra_notation.