# Coq Hello World

``````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.
``````

1 个赞

(* *) 之间的是注释，也是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 个赞

ocaml和prolog是同一类

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