Library inversion_automation

Inversion and Automation

Inversion


Section INVERSION.

Lemma inject_nat : forall n m :nat, S n = S m -> n = m.
Proof.
intros n m Heq.
inversion_clear Heq.
reflexivity.
Qed.

Print le.

Inductive le (n : nat) : nat -> Prop :=
le_n : n <= n
| le_S : forall m : nat, n <= m -> n <= S m

Check le_ind.

Lemma basic1 :forall n : nat, le n 0 -> n = 0.
Proof.
induction n.
auto.
intro H.
And now what??
inversion H.
inversion analyses the possible cases for H; there is none (!), because the types of le_n and le_S don't match on the type of H, so the type S n <= 0 is empty, so we can conclude everything, and we have a proof of S n = 0
Qed.

Different proof of the same lemma There is no need to do an induction on n
Lemma basic2 :forall n : nat, le n 0 -> n = 0.
Proof.
intros n H.
inversion H.
auto.
Qed.

Here you see what hypotheses inversion creates
Lemma explain_inversion : forall R : nat -> nat -> Prop, forall n m : nat, le n m -> R n m.
Proof.
intros R n m H.
inversion H.
inversion has created two goals, one for each case of the constructor of <= To see the second goal:
Show 2.
Abort.

Inductive even : nat -> Prop :=
| even_O : even O
| even_S_S : forall n, even n -> even (S (S n)).

Print even.

Lemma base1_even : ~ even 1.
Proof.
intro H.
inversion H.
Qed.

Lemma base3_even : ~ even 3.
Proof.
intro H.
inversion_clear H.
inversion H0.
also try: simple inversion H. inversion H0. inversion H1. intros H3. inversion H3. If you want to really understand what inversion H1 does here:
  • it applies even_ind with P:= fun n:nat => n=1 -> False
  • It then does all kinds of simplifications on the constraints to solve the goal
To see only the first step at work, do simple inversion H. Show 2. (to see the second goal that simple inversion H has created
Qed.

Lemma base2_even : forall n, ~ even n -> ~even (S (S n)).
Prove using inversion_clear
Admitted.

Inductive odd : nat -> Prop :=
| odd_1 : odd 1
| odd_S_S : forall n, odd n -> odd (S (S n)).

Lemma base1_odd : ~ odd 0.
Proof.
Admitted.

Lemma base2_odd : forall n, ~ odd n -> ~odd (S (S n)).
Proof.
Prove using inversion_clear
Admitted.

Print option.
Lemma option_eq : forall x y : nat, Some x = Some y -> x =y.
Proof.
intros x y H.
inversion H.
This derives x=y from Some x = Some y, which holds because Some is a constructor
reflexivity.
Qed.

Lemma option_eq1 : forall x : nat, Some x <> None.
Proof.
intro x.
intro H.
inversion H.
Qed.

End INVERSION.

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

Note that n ?= m abbreviates Nat.compare n m and n =? m abbreviates Nat.eqb n m
Case distinction on Nat.compare n m
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.
Proof.
intros n m.
unfold ThreeChoices.
case (n ?= m).
- auto.
- auto.
- auto.
Qed.