问题[coq](coding)

我正在尝试证明一个插入基于列表的优先级队列的正确性定理。以下是插入函数、归纳性质以及我正在使用的证明：

Fixpoint insert (x : nat) (l : list nat) : list nat :=
  match l with
  | [] => [x]
  | h :: t => if x <=? h then x :: h :: t else h :: insert x t
  end.

Inductive list_PQ_property : list nat -> Prop :=
| sorted_empty : list_PQ_property []
| sorted_one : forall x, list_PQ_property [x]
| sorted_add : forall x y l,
    x <= y ->
    list_PQ_property (y :: l) ->
    list_PQ_property (x :: y :: l).

Theorem insert_correctness :
  forall (pq : PQ) (x : el),
    list_PQ_property pq ->
    list_PQ_property (insert x pq).
Proof.
  intros pq x H.
  induction H as [ | y | a b l Hab IHl].
  - simpl. apply sorted_one.
  - simpl. destruct (x <=? y) eqn:E.
    + apply Nat.leb_le in E. apply sorted_add.
      * apply E.
      * apply sorted_one.
    + apply Nat.leb_gt in E.
      apply Nat.lt_le_incl in E.
      apply sorted_add.
      * apply E.
      * apply sorted_one.
  - simpl. destruct (x <=? a) eqn:E.
    + apply Nat.leb_le in E.
      apply sorted_add.
      * apply E.
      * apply sorted_add.
        -- apply Hab.
        -- apply IHl.
  + destruct (x <=? b) eqn:E'.
      * apply Nat.leb_le in E'.
      apply sorted_add.
      apply Nat.lt_le_incl.
      apply Nat.leb_gt in E. apply E.
      apply sorted_add.
        ++ apply E'.
        ++ apply IHl.
       * apply Nat.leb_gt in E'.
        apply sorted_add.
        -- apply Hab.
Admitted.

当我开始证明的时候，一切都很简单，直到我遇到第三个情况。一开始我卡在了

apply sorted_add.
        ++ apply E'.
        ++ apply IHl.

我的目标是 ，b <= x但我对 E' 的假设是 ，x <= b直到我通过应用 Coq 中的一堆 Nat 函数绕过了传递性。现在我卡在了 ，我的 IHIHl 假设如下所示： IHIHl : list_PQ_property (insert x (b :: l)) ，但我的目标是： list_PQ_property (b :: insert x l)。

我不知道如何解决这个问题，或者我是否正确地证明了这一点。

任何指导都将不胜感激。

欲了解更多信息，到目前为止我的完整目标是这样的：

1 goal
x : el
a, b : nat
l : list nat
Hab : a <= b
IHl : list_PQ_property (b :: l)
IHIHl : list_PQ_property (insert x (b :: l))
E : (x <=? a) = false
E' : b < x
______________________________________(1/1)
list_PQ_property (b :: insert x l)

我试过用 IHIHl，但没用。我有点迷茫，我猜这就是我建立证明的方法。

我在 中使用标准向量类型Coq.Vectors。我想证明关于 的以下属性shiftin。

Lemma vec_shiftin_eq:
  forall A (n:nat) (a0 a1: A) (t0 t1: t A n),
  shiftin a0 t0 = shiftin a1 t1 <-> a0 = a1 /\ t0 = t1.

<-很简单。 -> a0 = a1没问题。但我对 一无所知-> t0 = t1。

第 2 部分 （已添加）：
编辑：此部分现在作为单独的问题提出： shiftin、shiftout 和 last

同时，如果向量长度至少为 1，是否有可能证明last和shiftout是的有效反转？shiftin

Lemma shiftin_last_shiftout:
  forall A (n:nat) (x: t A (S n)),
  x = shiftin (last x) (shiftout x).

我非常熟悉在声明归纳类型时区分参数和索引。我不确定的是，在声明定理时，将内容放在冒号前和冒号后是否有区别。具体来说

Lemma par (n : nat) : n < 1 -> n = 0.

Lemma ind : forall (n : nat), n < 1 -> n = 0.

我发现的一个区别是，在证明 时par，冒号右侧的所有内容最初都在上下文中，而在 中则ind必须如此intro。您知道这两者之间还有其他区别吗？您能举一个例子来说明这不仅仅是一堆intro/revert吗？

我担心的问题之一是自动化可能会更喜欢其中一个，例如autorewrite或auto，尽管我找不到会产生影响的例子。

在以下证明脚本中：

Theorem foo : exists p, p = (1, 1).
Proof. eexists ?[p]. destruct ?p.

我们最终的目标是：

  n, n0 : nat
  ============================
  (n, n0) = (1, 1)

有没有一种方法可以让?p我们最终得到和 相同的目标？eexists (?[p1], ?[p2]).例如：eexists ?[p].

(?p1, ?p2) = (1, 1)

我有这个目标，我想证明这一点。

1 goal
t1, t2 : FCPLang
H : evalS t1 = Some t2
______________________________________(1/1)
evalBS t1 = evalBS t2

为了证明这一点，我使用了induction t1.，但这些是引入的归纳假设：

1 goal
t1_1, t1_2, t1_3, t2 : FCPLang
H : evalS (if_then_else t1_1 t1_2 t1_3) = Some t2
IHt1_1 : evalS t1_1 = Some t2 -> evalBS t1_1 = evalBS t2
IHt1_2 : evalS t1_2 = Some t2 -> evalBS t1_2 = evalBS t2
IHt1_3 : evalS t1_3 = Some t2 -> evalBS t1_3 = evalBS t2
______________________________________(1/1)
evalBS (if_then_else t1_1 t1_2 t1_3) = evalBS t2

我认为这毫无用处，因为t2再次使用它们，而不是引入一个新术语，例如： IHt1_1 : evalS t1_1 = Some t2_1 -> evalBS t1_1 = evalBS t2_1 我该如何解决这个问题？

考虑以下相互归纳命题

Inductive TypeA : Prop :=
  | ConstructorA : TypeB -> TypeA
with TypeB : Prop :=
  | ConstructorB : TypeA -> TypeB. 

以下是~TypeA函数式风格的证明

Fixpoint TypeA_is_empty' (a : TypeA) : False :=
  match a with 
  | ConstructorA b' => TypeB_is_empty' b'
  end
with TypeB_is_empty' (b : TypeB) : False :=
  match b with 
  | ConstructorB a' => TypeA_is_empty' a'
  end.

战术风格上如何证明~TypeA？

如果 Coq 中存在类似的东西，我希望能够将它们证明为相互定理

Theorem TypeA_is_empty : ~ TypeA.
Theorem TypeB_is_empty : ~ TypeB.
Proof.
  unfold not.
  intros b.
  inversion b as [a].
  apply (TypeA_is_empty a).
Qed.
Proof.
  unfold not.
  intros a.
  inversion a as [b].
  apply (TypeB_is_empty b).
Qed.

编辑：发现 Coq 有这样的相互定理语法，但它会抛出错误

Lemma TypeA_is_empty : ~ TypeA 
  with TypeB_is_empty : ~ TypeB.

**Cannot find common (mutual) inductive premises or coinductive conclusions in the statements.**

我在 Coq 中遇到了一个令人费解的情况，当时我正在处理关系和集合。我定义了它们之间的强制转换以及解决成员目标的策略：

Require Import Lia Reals Lra Classical_sets List Ensembles Relations_1.
Import ListNotations.

Notation "x ∈ A" := (In _ A x) (at level 40).
Notation "A ⋃ B" := (Union _ A B) (at level 30).
Notation "⦃⦄" := (Empty_set _).
Notation ℝ := R.

Fixpoint list_to_ensemble {U : Type} (l : list U) : Ensemble U :=
  match l with
  | [] => ⦃⦄
  | x :: xs => Union U (Singleton U x) (list_to_ensemble xs)
  end.

Notation "⦃ x ⦄" := (Singleton _ x).
Notation "⦃ x , y , .. , z ⦄" :=
  (@list_to_ensemble _ (cons x (cons y .. (cons z nil) ..)))
  (format "⦃ x , y , .. , z ⦄").

Lemma In_Union_def : forall (U : Type) (A B : Ensemble U) (x : U),
  x ∈ (A ⋃ B) <-> x ∈ A \/ x ∈ B.
Proof.
  intros; split; [apply Union_inv | intros [H1 | H1]; [apply Union_introl; auto | apply Union_intror; auto]].
Qed.

Coercion rel_to_ens {A} (R : Relation A) : Ensemble (A * A) := 
  fun p => R (fst p) (snd p).

Coercion ens_to_rel {A} (E : Ensemble (A * A)) : Relation A := 
  fun x y => E (x,y).

Lemma x_y_In_implies_rel : forall A (R : Relation A) x y, (x, y) ∈ R <-> R x y.
Proof.
  intros; split; auto.
Qed.

Ltac solve_in_Union :=
  simpl; auto;
  match goal with
  | [ |- ?x ∈ Singleton _ _ ] => 
      apply Singleton_intro; (try reflexivity; try nia; try nra)
  | [ |- ?x ∈ Union _ ?A ?B ] => 
      apply In_Union_def; solve [ left; solve_in_Union | right; solve_in_Union ]
  | [ |- ?G ] => fail "Goal not solvable"
  end.

在证明简单成员属性时：

Section Example.
  Open Scope R_scope.
  Let R : Relation ℝ := ⦃ (1,1),(1,2),(1,3),(1,4),(2,3),(2,5),(2,6),(3,5),(4,5),(4,6) ⦄.

  Lemma lemma_example : R 1 1.
  Proof.
    apply x_y_In_implies_rel. unfold R. try solve_in_Union.
    assert ((1, 1) ∈ ⦃ (1,1),(1,2),(1,3),(1,4),(2,3),(2,5),(2,6),(3,5),(4,5),(4,6) ⦄) as H1 by solve_in_Union.
    auto.
  Qed.
End Example.

当我尝试使用 trysolve_in_Union 解决目标时，我的目标正是：

(1, 1) ∈ ⦃(1,1),(1,2),(1,3),(1,4),(2,3),(2,5),(2,6),(3,5),(4,5),(4,6)⦄

奇怪的是，直接在此目标上使用solve_in_Union会失败。但是，如果我断言完全相同的目标文本并尝试使用solve_in_Union来证明它，它就会起作用：

更令人费解的是，如果我按照目标进行模式匹配并打印它：

match goal with
| [ |- ?G ] => idtac G
end.

它显示了与断言中有效的完全相同的文本。为什么solve_in_Union在原始目标上失败，但在相同目标的断言上却成功？这两种看似相同的情况之间的根本区别是什么？

至于我使用的 Coq 版本，当我在终端中输入 coqc -v 时，我得到

coqc -v Coq 证明助手，版本 8.19.2，使用 OCaml 5.2.0 编译

几个例子表明，目标中的矛盾（比如，当尝试对列表的长度进行归纳时，“0 > 0 意味着某事”）可以通过以下方式处理

exfalso. omega.

由于 Omega 模块已弃用，因此缺少 omega 策略。处理上述情况的正确方法是什么？

谢谢

作为 Coq 新手，我被这个问题难住了。希望有人能帮忙！

给定 Coq 中有限类型的编码如下 -

Fixpoint fin (n : nat) : Type :=
  match n with
  | 0 => False
  | S m => option (fin m)
  end.

是否可以定义一个函数，将值从 提升fin (S n)到fin (S (S n))，同时保持值不变。因此，我希望有以下等式，例如 -

@up 2 (None : fin 2) = (None : fin 3)

@up 2 (Some None : fin 2) = (Some None : fin 3)

我想写这个 -

Fixpoint up {n:nat} : fin (S n) -> fin (S (S n)) :=
fun p => match p with 
         | None => None 
         | Some p' => Some (up p)

但它被拒绝了。直观地，我明白这是可能的，因为 - 的成员fin 2 - None, Some None是 的成员fin 3 - None, Some None, Some (Some None)等等。但我无法为它编写函数。我怀疑这是因为递归定义必须处理@up 0应该有一个空匹配的地方，但我不确定如何编写这种情况。任何帮助都将不胜感激！谢谢

我想证明自然数中不等式的否定逆：

对于所有 ij：nat，i <= j -> 对于所有 w：nat，i <= w -> j <= w -> w - i >= w - j。

我尝试通过归纳法来证明。我首先w - i >= w - i通过反身性简单地证明。然后我尝试证明w - i >= w - S m只要有w - i >= w - m，我就会卡住。似乎如果我证明w - m >= w - S m，就完成了。但我也无法解决这个问题。有人能帮忙吗？非常感谢！

为什么网络上没有可用策略的简单列表及其描述？