Coq begginer here, how to understand the syntax?

Question

I recently started a class on my college where we solve logical problems in Coq. I'm having problems understanding the principles of programming in Coq, the syntax and "building" ideas in my brain when it comes to problems. For instance,

Definition orb_3 (x y : bool) : bool :=
match x, y with
  | false, false => false
  | _, _ => true
end.

This is the first function for defining disjunction, and

Definition orb (x y : bool) : bool :=
match x with
  | true => true
  | false => y
end.

is the second function for defining disjunction. They should give out the same result, for example orb3 true false should give out the result true. Same goes for orb true false.

Now, this code

Goal forall x y : bool, orb x y = orb_3 x y.
Proof.
  intros x y. destruct x.
  - destruct y.
    -- simpl. reflexivity.
    -- simpl. reflexivity.
  - destruct y ; simpl ; reflexivity.
Qed.

is the proof my professor wrote as proof that these two functions are equal. My question is: what does intros, destruct, simpl, reflexivity do? What is the general idea you should have in mind when doing proofs in Coq? Also, where can I find some useful, easy-to-understand Coq tutorials or literature?

Arthur Azevedo De Amorim Arthur Azevedo De Amorim · Accepted Answer · 2021-03-22T15:51:52

This question is a bit open ended; it's like asking what you should have in mind when programming in some programming language! There is plenty of material available on the internet on how to use Coq, which explains what the tactics intros, destruct etc. do. I particularly recommend the Software Foundations series, available here. It is long, but the first few chapters of the "Logical Foundations" volume should already give you a basic idea of what is going on.

Coq begginer here, how to understand the syntax?

1 Answers