Rocq (Coq) Lemma Search

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_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']

• 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_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']

• 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']

• SimpleC.EE.Applications_human.convex_hull.Andrew_Monotone_Chain.andrew_two_fan_cover_to_merged_max_weak : Lemma andrew_two_fan_cover_to_merged_max_weak : forall first last lower_mid upper_mid base, weak_rev_ccw_list first (rev upper_mid ++ last :: rev lower_mid) -> Forall (fun q => point_in_hull q (first :: rev upper_mid ++ [last]) \/ point_in_hull q (first :: last :: rev lower_mid)) base -> is_max_hull' first (rev upper_mid ++ last :: rev lower_mid) base
  Details

  Terms: ['Corelib.Init.Datatypes.cons', 'Corelib.Init.Datatypes.nil', 'SimpleC.EE.Applications_human.convex_hull.Maximality.point_in_hull', 'Corelib.Init.Datatypes.app', "SimpleC.EE.Applications_human.convex_hull.Maximality.is_max_hull'", 'SimpleC.EE.Applications_human.convex_hull.Convexity.weak_rev_ccw_list', 'Stdlib.Lists.List.rev']

  Inductive Types: ['Corelib.Lists.ListDef.Forall', 'Corelib.Init.Logic.or', 'SimpleC.EE.Applications_human.convex_hull.Geo_Point_Primitives.point']