小编lar*_*rsr的帖子

在软件基础IndProp.v中,要求一个人证明鸽子原则,并且可以使用被排除的中间人,但是提到它并不是绝对必要的.我一直试图在没有EM的情况下证明它,但我的大脑似乎是经典的.

问:如何在不使用排除中间的情况下证明该定理？一般来说,如果没有可判定的平等,人们通常会如何处理类型的证据？

我很高兴看到一个完整的证据,但请避免"明确地"发布它,以免破坏软件基础课程的练习.

该定义使用两个归纳谓词,In和 repeats.

Require Import Lists.List.
Import ListNotations.

Section Pigeon.

  Variable (X:Type).
  Implicit Type (x:X).

  Fixpoint In x l : Prop :=                        (***    In       ***)
    match l with
    | nil => False
    | (x'::l') => x' = x \/ In x l'
    end.

  Hypothesis in_split : forall x l, In x l ->  exists l1 l2, l = l1 ++ x :: l2.
  Hypothesis in_app: …

在一个证明中我需要表明"如果n不是三的倍数,那么n + n也不是三的倍数." 我认为我的证据太长而且不太优雅.是否有一些更漂亮的写作方式？有没有ssreflect？(我确定在ssreflect中有一个oneliner :)).

我的证据n以三步为单位进行归纳.

Require Import Omega.
Lemma math_helper n: forall k, (forall q, n <> q * 3) ->  n + n <> k * 3.
  (* name the predicate Q and strengthen induction hypothesis *)
  pattern n; match goal with [ _:_ |- ?P ?n] => let X := fresh Q in remember P as X end.
  enough (Q n /\ Q (1+n) /\ Q (2+n)) by tauto.
  induction n; …

我可以证明以下内容Coq吗？

Lemma bool_uip (H1 : true = true): H1 = eq_refl true.

即所有证据true = true都相同？

例如,从它开始 forall c (H1 H2: c = true), H1 = H2.

不必添加任何公理(如UIP)会很高兴.我发现以下线程表明可能是这种情况:

在COQ中证明平等是反身性

我试图less_than在Coq中证明一些定理.我正在使用这个归纳定义:

Inductive less_than : nat->nat->Prop :=
   | lt1 : forall a, less_than O (S a)
   | lt2 : forall a b, less_than a b -> less_than a (S b)
   | lt3 : forall a b, less_than a b -> less_than (S a) (S b).

我总是需要显示lt3的倒数,

Lemma inv_lt3, forall a b, less_than (S a) (S b) -> less_than a b.
Proof.
   ???

我被困住了,如果有人对如何继续进行提示,我将非常感激.

(我的归纳定义是否有问题less_than？)

谢谢!

我需要证明该方程组没有解决方案（原因是它被过度确定）。在Coq中有一种简单的方法吗？是战术还是图书馆？

Require Import Reals.
Open Scope R.

Lemma no_solution:
  forall 
    b11 b12 b13 b14 b21 b22 b23 b24 b31 b32 b33 b34
    r r0 r1 r2 r3 r4 r5 r6 r7 r8 r9 r10 : R,
   1 = r * b11 + r0 * b21 + r1 * b31    ->
   0 = r * b12 + r0 * b22 + r1 * b32    ->
   0 = r * b13 + r0 * b23 + r1 * b33    -> …