我正在嘗試使用可以輕鬆生成的術語(在此特定示例中,從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