我正在尝试使用可以轻松生成的术语（在此特定示例中，从tauto）实例化存在量词的策略。我第一次尝试： Ltac mytac :=
match goal with
| |- (exists (_ : ?X), _) => cut X;
[ let t := fresh "t" in intro t ; exists t; firstorder
总之，这可能吗？ 我试图证明取消在一个组中工作。 我 a, b, x : G
H: a <+> x = b <+> x
，我想证明 a = b
我的想法是让一个假设 H2: a <+> x <+> i x = a <+> x <+> i x
（i是反函数）。 我已经试过 pose proof eq_refl (a <+> x <+> i x) as H.
但这似乎并没有工作。
我需要推理向量在Coq中的置换。标准库仅包含列表的排列定义。正如我的第一次尝试，我试图模仿它的载体： Inductive VPermutation: forall n, vector A n -> vector A n -> Prop :=
| vperm_nil: VPermutation 0 [] []
| vperm_skip {n} x l l' : VPermutat
我想通过Coq中的两个参数定义一个嵌套的递归函数。 Require Import List.
Import ListNotations.
Fixpoint map_sequence2 {A B C : Set} (f : A -> B -> option C)
(xs : list A) (ys : list B) : option (list C) :=
match xs, y