Library inductive_examples

Inductive Types

Booleans

Check bool.
Print bool.

Check bool_ind.

Definition neg (b : bool) : bool :=
match b with
true => false
| false => true
end.

Print neg.

There is some useful syntactic sugar for the type bool

Definition negg (b : bool) := if b then false else true.

Print negg.

Lemma bool1 : forall b : bool, neg (neg b) = b.
Proof.
intro b.
destruct b.

or elim b or case b

- simpl. reflexivity.
- simpl. reflexivity.

or chain the last 5 lines into destruct b; simpl; reflexivity.

Qed.

Distinct constructors of an inductive type are different: true and false are different
There is a simple tactic congruence that proves -- among other things -- that distinct constructors of an inductive type are different:

Lemma dist : ~ true = false.
Proof.
congruence.
Qed.

Natural Numbers

Print nat.
Print plus.

To define plus, we would type the following

Fixpoint plus' (n m : nat) {struct n} : nat :=
  match n with
  | O => m
  | S p => S (plus' p m)
  end.

Print plus'.

Lemma nat1 : forall n : nat, plus n 0 = n.
Proof.
intro n.
induction n.

Also try destruct n and notice it doesn't work: destruct only does a case analysis, but doesn't give you an induction hypothesis

- simpl.
  reflexivity.
- simpl.
  rewrite IHn.
  reflexivity.
Qed.

Print plus.

Lemma nat2 : forall n : nat, plus 0 n = n.
Proof.
simpl.

Note: this works because plus is defined by recursion over the first argument:
plus 0 n = n
plus (S m) n = S(plus m n)

auto.
Qed.

Exercise 1:
(a) Define plus'' by recursion over the second argument
(b) Prove forall n : nat, plus'' n 0 = n by a simple script as in Lemma nat2

Logical connectives are also defined as inductive types

Print True.
Print False.

False is the inductive type with no constructors

Check False_ind.

Lemma False1 : forall A:Prop, False -> A.
Proof.
intros A HF.

contradiction.

destruct HF.
Qed.

Check False_ind.

Print and.

conj : A -> B -> A /\ B is conjunction introduction

Check and_ind.

and_ind : forall A B P : Prop, (A -> B -> P) -> A /\ B -> P
is a generalised form of conjunction elimination.
We use split for introduction, destruct for elimination.

Print or.
Check or_ind.

Lemma triv1 :forall A B :Prop, A /\ B -> A \/B.
Proof.
intros A B.
intro H.
destruct H.

or induction H. or case H. or elim H.

left.
exact H.
Qed.

Lemma triv2 :forall A B C :Prop, (A ->C ) \/ (B ->C ) -> A /\B -> C.
Proof.
intros A B C H1 H2.
destruct H1.
- destruct H2.
  apply H; auto.
- apply H.
  destruct H2.
  auto.
Qed.

Example of a wrong Fixpoint definition! Try to feed this to Coq

Fixpoint f (n : nat) {struct n} : nat :=  
   match n with 
   | 0   => 0 
   | S p => f (f p)
end.

Example of a wrong Inductive definition! Try to feed this to Coq

Inductive Lambda : Set :=
  | var : nat -> Lambda
  | app : Lambda -> Lambda -> Lambda
  | abs : (Lambda -> Lambda) -> Lambda.