(* Various Examples of Programming and Proving in Coq IV *)
(** Automation and some goodies **)
(* Automation tactics:
intuition general
firstorder general
auto first do Require Import Arith, general, also solves basic arithmetic
ring solves equations over rings, basically nat with * + 0 1
lia first do Require Import Lia solves various kinds of equations and inequations over nat
congruence solves equations between closed terms and knows that constructors are different!
so apply to prove None < > Some t !!
*)
Require Import Arith.
Require Import Lia.
Lemma test_ring : forall x y z : nat, z * y + x * x *(y + z) = y * (z + x * x) + z * x * x.
Proof.
intros x y z.
ring.
(* lia can also solve this! *)
Qed.
Lemma test_lia : forall x y z : nat, 2 * (x + y) + z < z + 2 * x + y * 2 + 1.
Proof.
intros x y z.
lia.
(* ring cannot solve this, as it only solves equations *)
Qed.
Lemma test_intuition : forall A B C: Prop, (A -> B) /\ (B->C) -> A -> C.
Proof.
intros.
intuition.
(* tauto. also solves this; it is a complete proposition logic prover
for intuitionistic proposition logic *)
Qed.
Lemma test_intuition' : forall A B C D: Prop, (A -> B) /\ (B->C) -> (A \/ D) -> (C/\D).
Proof.
intros.
intuition.
(* intuition simplifies the statement, leaving the user with the
work that's still left to do. In this case, the goal is unprovable
so we are stuck, but in many cases this is very useful, as it does
all the trivial logical simplifications one has to do by hand otherwise
NB tauto. simply fails here
*)
Abort.
Section FirstOrder.
Variable D:Set.
Variable P Q : D -> D -> Prop.
Lemma test_firstorder: (forall x y :D, P x x -> Q x y ) -> forall x, P x x -> Q x x.
Proof.
firstorder.
(* firstorder is an experimental extension of tauto to first order logic *)
Qed.
End FirstOrder.
(* Defining functions over nat by case distinction *)
Inductive tree : Set :=
| leaf : tree
| node : tree -> nat -> tree -> tree.
(* When inserting an element in a tree we need to distinguish
n < m \/ n = m \/ m < n
There are various ways [basically 3] to do that
*)
(* 1. leb : nat -> nat -> bool *)
Print leb.
Print Nat.leb.
Check leb.
Definition test1 (n:nat):= if leb n 3 then 7 else 0.
(* Or with nice notation *)
Definition test2 (n:nat):= if n <=? 3 then 7 else 0.
(* 2. le_gt_dec : nat -> nat -> sumbool *)
Check le_gt_dec.
Print le_gt_dec.
Print sumbool.
Definition test3 (n:nat):= match le_gt_dec n 3 with
| left _ => 7
| right _ => 0
end.
(* Or in simpler notation: *)
Definition test4 (n:nat):= if le_gt_dec n 3 then 7 else 0.
(* So the if _ then _ else _ notation also works for sumbool instead of bool *)
(* 3. Nat.Compare : nat -> nat -> comparison *)
Print Nat.compare.
Check Nat.compare.
Print comparison.
(** Helper axioms to deal with nat comparisons in Coq. *)
Lemma comp_lt :
forall n m : nat, (Nat.compare n m) = Lt -> n < m.
Proof.
intros.
(* And now what?? *)
Search Nat.compare.
(* Gives you all the basic lemmas about Nat.compare *)
Search "?=".
apply nat_compare_Lt_lt.
assumption.
Qed.
(** Case distinction on nat_compare *)
Definition ThreeChoices (n m : nat) : nat :=
match Nat.compare n m with
| Lt => 0
| Eq => 1
| Gt => 2
end.
Lemma simple : forall n m : nat, ThreeChoices n m <= 2.
Proof.
intros n m.
(* And now what ??
destruct (Nat.compare n m) doesn't work
elim (nat_compare n m) doesn't work ... *)
(* Solution: use "eqn:" to keep the equation you destruct:
destruct (Nat.compare n m) eqn:Heqe. *)
(* ==> Alternative solution: case_eq (Nat.compare n m). <== *)
destruct (Nat.compare n m) eqn:Heqe.
unfold ThreeChoices.
rewrite Heqe.
auto.
unfold ThreeChoices.
rewrite Heqe.
auto.
(* etcetera *)
Admitted.
(* An alernative way that helps in this simple case *)
Lemma simple' : forall n m : nat, ThreeChoices n m <= 2.
intros n m.
unfold ThreeChoices.
case (n ?= m).
- auto.
- auto.
- auto.
Qed.