Coq Hello World

闲聊灌水
1 
Theorem andb_true_elim2 : forall b c : bool,
    andb b c = true -> c = true.

Proof.
  intros b c H.
  apply andb_prop with (a:=b )(b:=c) .
  assumption.
Qed.
2

讲 解 一 下

1 个赞
3

(* *) 之间的是注释，也是coq推理（希望这个词正确）的步骤。

Theorem andb_true_elim2 : forall b c : bool,
    andb b c = true -> c = true.

(*
1 subgoal (ID 182)

  ============================
  forall b c : bool, b && c = true -> c = true
*)

Proof.

  intros b c H.
(*
1 subgoal (ID 185)

  b, c : bool
  H : b && c = true
  ============================
  c = true
*)

  Search "andb_prop".
(*
andb_prop_elim: forall a b : bool, Is_true (a && b) -> Is_true a /\ Is_true b
andb_prop_intro:
  forall b1 b2 : bool, Is_true b1 /\ Is_true b2 -> Is_true (b1 && b2)
andb_prop: forall a b : bool, a && b = true -> a = true /\ b = true
*)

  apply andb_prop with (a:=b )(b:=c) .
(*
1 subgoal (ID 189)

  b, c : bool
  H : b && c = true
  ============================
  b && c = true
 *)

 assumption.
  (* No more subgoals. *)
Qed. 
(* OK *)
1 个赞
4

大致的意思就是（主要是我也不了解）

通过查找已有证明来证明现在的证明

5

萌新一脸蒙比

6

这个coq和prolog是同一类的语言吗？

7

ocaml和prolog是同一类

8

我觉得这个比“软件基础”更容易入门

https://cel.archives-ouvertes.fr/inria-00001173v6/document