proposition: Lemma Rnorm_eq invb (F : ringType) (f f' : bool -> Z -> F) zero add opp sub one mul exp inv : f =2 f' -> forall (R : semiRingType) (env : R -> F) e, Rnorm f zero add opp sub one mul exp inv invb env e = Rnorm f' zero add opp sub one mul exp inv invb env e.
proof: Proof. move=> ff' R m e. pose P R e := forall f f' invb (m : R -> F), f =2 f' -> Rnorm f zero add opp sub one mul exp inv invb m e = Rnorm f' zero add opp sub one mul exp inv invb m e. pose P0 V e := forall f f' invb (m : V -> F), f =2 f' -> Mnorm f zero add opp sub one mul exp inv invb m e = Mnorm f' zero add opp sub one mul exp inv invb m e. move: f f' invb m ff'. elim e using (@RExpr_ind' P P0); rewrite {R e}/P {}/P0 /=. - by []. - move=> R e1 IHe1 e2 IHe2 f f'. by case=> m ff'; [congr inv|]; (congr add; [exact: IHe1|exact: IHe2]). - move=> e1 IHe1 e2 IHe2 f f'. by case=> m ff'; [congr inv|]; (congr add; [exact: IHe1|exact: IHe2]). - move=> e1 IHe1 e2 IHe2 f f'. by case=> m ff'; [congr inv|]; (congr add; [exact: IHe1|exact: IHe2]). - move=> e1 IHe1 e2 IHe2 f f'. by case=> m ff'; [congr inv|]; (congr add; [exact: IHe1|exact: IHe2]). - move=> R e1 IHe1 e2 IHe2 f f' invb m ff'. by congr mul; [exact: IHe1|exact: IHe2]. - by move=> R e1 IHe1 f f' invb m ff'; congr opp; exact: IHe1. - by move=> e1 IHe1 f f' invb m ff'; congr opp; exact: IHe1. - move=> e1 IHe1 e2 IHe2 f f'. by case=> m ff'; [congr inv|]; (congr sub; [exact: IHe1|exact: IHe2]). - move=> R e1 IHe1 e2 IHe2 f f' invb m ff'. by congr mul; [exact: IHe1|exact: IHe2]. - by []. - move=> R e1 IHe1 e2 IHe2 f f' invb m ff'. by congr mul; [exact: IHe1|exact: IHe2]. - move=> e1 IHe1 e2 IHe2 f f' invb m ff'. by congr mul; [exact: IHe1|exact: IHe2]. - move=> e1 IHe1 e2 IHe2 f f' invb m ff'. by congr mul; [exact: IHe1|exact: IHe2]. - move=> e1 IHe1 e2 IHe2 f f' invb m ff'. by congr mul; [exact: IHe1|exact: IHe2]. - by move=> R e1 IHe1 n f f' invb m ff'; congr exp; exact: IHe1. - by move=> R e1 IHe1 n f f' invb m ff'; congr exp; exact: IHe1. - by move=> R e1 IHe1 n f f' invb m ff'; congr exp; exact: IHe1. - by move=> e1 IHe1 n f f' invb m ff'; congr exp; exact: IHe1. - by move=> e1 IHe1 n f f' invb m ff'; congr exp; exact: IHe1. - by move=> e1 IHe1 [|p|//] f f' invb m ff'; congr exp; exact: IHe1. - by move=> R e1 IHe1 f f' invb m ff'; apply: IHe1. - move=> p e IHe f f'. by case=> m ff'; [congr inv|]; congr add; rewrite ?ff'//; exact: IHe. - by move=> n f f' invb m ff'; rewrite /Rnorm ff'. - by move=> e IHe f f' invb m ff'; exact: IHe. - by move=> e IHe f f' [] m ff'; [congr inv|]; congr opp; congr add; exact: IHe. - by move=> n f f' invb m ff'; rewrite /Rnorm ff'. - by move=> n f f' invb m ff'; rewrite /Rnorm ff'. - by move=> R' R g e IHe f f' invb m ff'; exact: IHe. - by move=> R g e IHe f f' invb m ff'; exact: IHe. - by move=> R g e IHe f f' invb m ff'; exact: IHe. - by move=> R g e IHe f f' invb m ff'; exact: IHe. - by move=> R g e IHe f f' invb m ff'; exact: IHe. - by move=> V R g e IHe f f' invb m ff'; exact: IHe. - by move=> R g e IHe f f' invb m ff'; congr mul; exact: IHe. - by move=> R g e IHe f f' invb m ff'; congr mul; exact: IHe. - by move=> R g e IHe f f' invb m ff'; congr mul; exact: IHe. - by move=> R g e IHe f f' invb m ff'; congr mul; exact: IHe. - by []. - by []. - move=> V e1 IHe1 e2 IHe2 f f'. by case=> m ff'; [congr inv|]; (congr add; [exact: IHe1|exact: IHe2]). - move=> V e1 IHe1 e2 IHe2 f f' invb m ff'. by congr mul; [exact: IHe1|exact: IHe2]. - by move=> V e IHe f f' invb m ff'; congr opp; exact: IHe. - move=> V e1 IHe1 e2 IHe2 f f' invb m ff'. by congr mul; [exact: IHe1|exact: IHe2]. - by move=> V V' g e IHe f f' invb m ff'; exact: IHe. - by move=> V g e IHe f f' invb m ff'; congr mul; exact: IHe. - by move=> V g e IHe f f' invb m ff'; congr mul; exact: IHe. - by move=> V g e IHe f f' invb m ff'; congr mul; exact: IHe. - by move=> V g e IHe f f' invb m ff'; congr mul; exact: IHe. - by []. Qed.
imports: elpi(elpi) Coq(QArith) Coq.micromega(OrderedRing RingMicromega) mathcomp(all_ssreflect ssralg ssrnum ssrint) mathcomp.zify(ssrZ zify)