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

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

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

• 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.Vectors.VectorSpec.rev_nil : Lemma rev_nil A : rev (nil A) = []
  Details

  Terms: ['Stdlib.Vectors.VectorDef.nil', 'Stdlib.Vectors.VectorDef.rev', 'Corelib.Init.Datatypes.O']

  Inductive Types: ['Corelib.Init.Logic.eq', 'Stdlib.Vectors.VectorDef.t']

• Stdlib.Numbers.HexadecimalFacts.rev_rev : Lemma rev_rev d : rev (rev d) = d
  Details

  Terms: ['Corelib.Init.Hexadecimal.rev']

  Inductive Types: ['Corelib.Init.Logic.eq', 'Corelib.Init.Hexadecimal.uint']

• Stdlib.Numbers.DecimalFacts.rev_rev : Lemma rev_rev d : rev (rev d) = d
  Details

  Terms: ['Corelib.Init.Decimal.rev']

  Inductive Types: ['Corelib.Init.Decimal.uint', 'Corelib.Init.Logic.eq']

• Stdlib.MSets.MSetGenTree.Props.Props.rev_elements_rev : Lemma rev_elements_rev s : rev_elements s = rev (elements s)
  Details

  Terms: ['M.rev_elements', 'M.elements', 'Stdlib.Lists.List.rev']

  Inductive Types: ['Corelib.Init.Logic.eq', 'Corelib.Init.Datatypes.list']

• Stdlib.Numbers.HexadecimalNat.Unsigned.Unsigned.to_uint_alt : Lemma to_uint_alt n : Nat.to_hex_uint n = rev (to_lu n)
  Details

  Terms: ['Corelib.Init.Hexadecimal.rev', 'Stdlib.Arith.PeanoNat.Nat.to_hex_uint', 'Stdlib.Numbers.HexadecimalNat.Unsigned.to_lu']

  Inductive Types: ['Corelib.Init.Logic.eq', 'Corelib.Init.Hexadecimal.uint']

• Stdlib.Numbers.DecimalNat.Unsigned.Unsigned.to_uint_alt : Lemma to_uint_alt n : Nat.to_uint n = rev (to_lu n)
  Details

  Terms: ['Stdlib.Numbers.DecimalNat.Unsigned.to_lu', 'Stdlib.Arith.PeanoNat.Nat.to_uint', 'Corelib.Init.Decimal.rev']

  Inductive Types: ['Corelib.Init.Decimal.uint', 'Corelib.Init.Logic.eq']

• Stdlib.Lists.List.Facts.length_app : Lemma length_app : forall l l' : list A, length (l ++ l') = length l + length l'
  Details

  Terms: ['Corelib.Init.Nat.add', 'Corelib.Init.Datatypes.length', 'Corelib.Init.Datatypes.app']

  Inductive Types: ['Corelib.Init.Datatypes.nat', 'Corelib.Init.Logic.eq', 'Corelib.Init.Datatypes.list']

• Stdlib.Numbers.DecimalFacts.length_lnzhead : Lemma length_lnzhead l : length (lnzhead l) <= length l
  Details

  Terms: ['Corelib.Init.Datatypes.length', 'Stdlib.Numbers.DecimalFacts.lnzhead']

  Inductive Types: ['Stdlib.Numbers.DecimalFacts.digits', 'Corelib.Init.Peano.le']

• Stdlib.Numbers.HexadecimalFacts.length_lnzhead : Lemma length_lnzhead l : length (lnzhead l) <= length l
  Details

  Terms: ['Stdlib.Numbers.HexadecimalFacts.lnzhead', 'Corelib.Init.Datatypes.length']

  Inductive Types: ['Corelib.Init.Peano.le', 'Stdlib.Numbers.HexadecimalFacts.digits']

• Stdlib.Lists.List.Bool.partition_length : Theorem partition_length l l1 l2 : partition l = (l1, l2) -> length l = length l1 + length l2
  Details

  Terms: ['Corelib.Init.Nat.add', 'Corelib.Init.Datatypes.pair', 'Corelib.Init.Datatypes.length', 'Stdlib.Lists.List.Bool.partition']

  Inductive Types: ['Corelib.Init.Datatypes.nat', 'Corelib.Init.Logic.eq', 'Corelib.Init.Datatypes.list', 'Corelib.Init.Datatypes.prod']

• Stdlib.Lists.List.ListOps.rev_alt : Lemma rev_alt : forall l, rev l = rev_append l []
  Details

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

  Inductive Types: ['Corelib.Init.Logic.eq', 'Corelib.Init.Datatypes.list']

• Stdlib.Numbers.HexadecimalFacts.rev_nztail_rev : Lemma rev_nztail_rev d : rev (nztail (rev d)) = nzhead d
  Details

  Terms: ['Corelib.Init.Hexadecimal.rev', 'Corelib.Init.Hexadecimal.nzhead', 'Stdlib.Numbers.HexadecimalFacts.nztail']

  Inductive Types: ['Corelib.Init.Logic.eq', 'Corelib.Init.Hexadecimal.uint']

• Stdlib.Numbers.DecimalFacts.rev_nztail_rev : Lemma rev_nztail_rev d : rev (nztail (rev d)) = nzhead d
  Details

  Terms: ['Corelib.Init.Decimal.nzhead', 'Stdlib.Numbers.DecimalFacts.nztail', 'Corelib.Init.Decimal.rev']

  Inductive Types: ['Corelib.Init.Decimal.uint', 'Corelib.Init.Logic.eq']

• Stdlib.Numbers.HexadecimalFacts.rev_lnorm_rev : Lemma rev_lnorm_rev d : rev (lnorm (rev d)) = unorm d
  Details

  Terms: ['Corelib.Init.Hexadecimal.rev', 'Corelib.Init.Hexadecimal.unorm', 'Stdlib.Numbers.HexadecimalFacts.lnorm']

  Inductive Types: ['Corelib.Init.Logic.eq', 'Corelib.Init.Hexadecimal.uint']

• Stdlib.Numbers.DecimalFacts.rev_lnorm_rev : Lemma rev_lnorm_rev d : rev (lnorm (rev d)) = unorm d
  Details

  Terms: ['Stdlib.Numbers.DecimalFacts.lnorm', 'Corelib.Init.Decimal.rev', 'Corelib.Init.Decimal.unorm']

  Inductive Types: ['Corelib.Init.Decimal.uint', 'Corelib.Init.Logic.eq']