Rocq (Coq) Lemma Search

Definition

Result

Stdlib.Lists.List.ListOps.rev_app_distr : Lemma rev_app_distr : forall x y : list A, rev (x ++ y) = rev y ++ rev x

Details

Terms: ['Stdlib.Lists.List.ListOps.rev', 'Corelib.Init.Datatypes.app']

Inductive Types: ['Corelib.Init.Logic.eq', 'Corelib.Init.Datatypes.list']
Equations.Examples.Basics.rev_app : Lemma rev_app : forall {A} (l l' : list A), rev (l ++ l') = rev l' ++ rev l

Details

Terms: ['Equations.Examples.Basics.rev', 'Equations.Examples.Basics.app']

Inductive Types: ['Corelib.Init.Logic.eq', 'Corelib.Init.Datatypes.list']
Stdlib.Lists.List.ListOps.rev_inj : Lemma rev_inj (l1 l2 : list A) : rev l1 = rev l2 -> l1 = l2

Details

Terms: ['Stdlib.Lists.List.ListOps.rev']

Inductive Types: ['Corelib.Init.Logic.eq', 'Corelib.Init.Datatypes.list']
Stdlib.Lists.List.ListOps.rev_unit : Remark rev_unit : forall (l : list A) (a : A), rev (l ++ [a]) = a :: rev l

Details

Terms: ['Corelib.Init.Datatypes.nil', 'Stdlib.Lists.List.ListOps.rev', 'Corelib.Init.Datatypes.cons', 'Corelib.Init.Datatypes.app']

Inductive Types: ['Corelib.Init.Logic.eq', 'Corelib.Init.Datatypes.list']
Stdlib.Lists.List.ListOps.rev_involutive : Lemma rev_involutive : forall l : list A, rev (rev l) = l

Details

Terms: ['Stdlib.Lists.List.ListOps.rev']

Inductive Types: ['Corelib.Init.Logic.eq', 'Corelib.Init.Datatypes.list']
Stdlib.Lists.List.Bool.filter_rev : Lemma filter_rev (l : list A) : filter (rev l) = rev (filter l)

Details

Terms: ['Stdlib.Lists.List.Bool.filter', 'Stdlib.Lists.List.rev']

Inductive Types: ['Corelib.Init.Logic.eq', 'Corelib.Init.Datatypes.list']
Equations.Examples.Equations_Tutorial_VeriMag.BuildingUp.BuildingUp.rev_acc_eq : Lemma rev_acc_eq : forall {A} (l : list A), rev_acc l = rev l

Details

Terms: ['Equations.Examples.Equations_Tutorial_VeriMag.BuildingUp.rev_acc', 'Equations.Examples.Equations_Tutorial_VeriMag.BuildingUp.rev']

Inductive Types: ['Corelib.Init.Logic.eq', 'Corelib.Init.Datatypes.list']
Equations.Examples.accumulator.rev_acc_eq : Lemma rev_acc_eq : forall {A} (l : list A), rev_acc l = rev l

Details

Terms: ['Equations.Examples.accumulator.rev_acc', 'Stdlib.Lists.List.rev']

Inductive Types: ['Corelib.Init.Logic.eq', 'Corelib.Init.Datatypes.list']
Equations.Examples.Basics.rev_rev_acc : Lemma rev_rev_acc : forall {A} (l : list A), rev_acc l [] = rev l

Details

Terms: ['Corelib.Init.Datatypes.nil', 'Equations.Examples.Basics.rev', 'Equations.Examples.Basics.rev_acc']

Inductive Types: ['Corelib.Init.Logic.eq', 'Corelib.Init.Datatypes.list']
mathcomp.ssreflect.seq.Sequences.rev_cat : Lemma rev_cat s t : rev (s ++ t) = rev t ++ rev s

Details

Terms: ['Corelib.Init.Datatypes.nil', 'mathcomp.ssreflect.seq.Sequences.cat', 'mathcomp.ssreflect.seq.Sequences.catrev', 'mathcomp.ssreflect.seq.Sequences.rev']

Inductive Types: ['Corelib.Init.Logic.eq', 'Corelib.Init.Datatypes.list']
CoRN.fta.CPoly_Rev.Poly_Reverse.Rev_plus : Lemma Rev_plus : forall p1 p2 n, Rev n (p1 [+] p2) [=] Rev n p1 [+] Rev n p2

Details

Terms: ['CoRN.fta.CPoly_Rev.Poly_Reverse.Rev', 'CoRN.algebra.CSetoids.csbf_fun', 'CoRN.algebra.RSetoid.st_eq', 'CoRN.algebra.CSemiGroups.csg_op']

Inductive Types: ['Corelib.Init.Datatypes.nat']
mathcomp.ssreflect.seq.EqSeq.rev_pivot : Lemma rev_pivot x s1 s2 : rev (s1 ++ x :: s2) = rev s2 ++ x :: rev s1

Details

Terms: ['mathcomp.ssreflect.eqtype.Equality.sort', 'mathcomp.ssreflect.seq.rev', 'Corelib.Init.Datatypes.cons', 'mathcomp.ssreflect.seq.cat']

Inductive Types: ['Corelib.Init.Logic.eq', 'Corelib.Init.Datatypes.list']
CoRN.fta.CPoly_Rev.Poly_Reverse.Rev_minus : Lemma Rev_minus : forall p1 p2 n, Rev n (p1 [-] p2) [=] Rev n p1 [-] Rev n p2

Details

Terms: ['CoRN.fta.CPoly_Rev.Poly_Reverse.Rev', 'CoRN.algebra.CGroups.cg_minus', 'CoRN.algebra.RSetoid.st_eq']

Inductive Types: ['Corelib.Init.Datatypes.nat']
Stdlib.Lists.List.ListOps.rev_eq_app : Lemma rev_eq_app : forall l l1 l2, rev l = l1 ++ l2 -> l = rev l2 ++ rev l1

Details

Terms: ['Stdlib.Lists.List.ListOps.rev', 'Corelib.Init.Datatypes.app']

Inductive Types: ['Corelib.Init.Logic.eq', 'Corelib.Init.Datatypes.list']
mathcomp.ssreflect.seq.Flatten.rev_flatten : Lemma rev_flatten ss : rev (flatten ss) = flatten (rev (map rev ss))

Details

Terms: ['mathcomp.ssreflect.seq.Flatten.flatten', 'mathcomp.ssreflect.seq.rev', 'mathcomp.ssreflect.seq.map']

Inductive Types: ['Corelib.Init.Logic.eq', 'Corelib.Init.Datatypes.list']
mathcomp.ssreflect.seq.Sequences.rev_rcons : Lemma rev_rcons s x : rev (rcons s x) = x :: rev s

Details

Terms: ['Corelib.Init.Datatypes.nil', 'mathcomp.ssreflect.seq.Sequences.cat', 'Corelib.Init.Datatypes.cons', 'mathcomp.ssreflect.seq.Sequences.rev']

Inductive Types: ['Corelib.Init.Logic.eq', 'Corelib.Init.Datatypes.list']
Stdlib.Vectors.VectorSpec.rev_shiftin : Lemma rev_shiftin A : forall a n (v : t A n), rev (shiftin a v) = a :: rev v

Details

Terms: ['Stdlib.Vectors.VectorDef.cons', 'Stdlib.Vectors.VectorDef.rev', 'Corelib.Init.Datatypes.S', 'Stdlib.Vectors.VectorDef.shiftin']

Inductive Types: ['Corelib.Init.Datatypes.nat', 'Corelib.Init.Logic.eq', 'Stdlib.Vectors.VectorDef.t']
CoRN.fta.CPoly_Rev.Poly_Reverse.Rev_mult : Lemma Rev_mult : forall n1 n2 p1 p2, degree_le n1 p1 -> degree_le n2 p2 -> Rev (n1 + n2) (p1 [*] p2) [=] Rev n1 p1 [*] Rev n2 p2

Details

Terms: ['CoRN.fta.CPoly_Rev.Poly_Reverse.Rev', 'CoRN.algebra.CPoly_Degree.degree_le', 'Corelib.Init.Nat.add', 'CoRN.algebra.CSetoids.csbf_fun', 'CoRN.algebra.CRings.cr_mult', 'CoRN.algebra.RSetoid.st_eq']

Inductive Types: ['Corelib.Init.Datatypes.nat']
mathcomp.ssreflect.seq.Sequences.revK : Lemma revK : involutive rev

Details

Terms: ['Corelib.Init.Datatypes.nil', 'mathcomp.ssreflect.seq.Sequences.rev']

Inductive Types: ['Corelib.Init.Logic.eq', 'Corelib.Init.Datatypes.list']
CoRN.fta.CPoly_Rev.Poly_Reverse.Rev_sum0 : Lemma Rev_sum0 : forall a_ l n, Rev n (Sum0 l a_) [=] Sum0 l (fun i => Rev n (a_ i))

Details

Terms: ['CoRN.fta.CPoly_Rev.Poly_Reverse.Rev', 'CoRN.algebra.CSums.Sum0', 'CoRN.algebra.RSetoid.st_eq']

Inductive Types: ['Corelib.Init.Datatypes.nat']