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

讲 解 一 下


#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 *)


#4

大致的意思就是(主要是我也不了解)

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


#5

萌新一脸蒙比


#6

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


#7

ocaml和prolog是同一类


#8

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

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