bst as an inductive proposition

Our bst fixpoint from Lab 2 could be equivalently rewritten as an inductive proposition:

Inductive tree : Set :=
| Leaf
| Node (l : tree) (n : nat) (r : tree).

Inductive bst : tree -> (nat -> Prop) -> Prop :=
| bst_leaf :
  forall s (s_empty : forall x, ~s x),
    bst Leaf s
| bst_node :
  forall s tl d tr
    (left_bst  : bst tl (fun x => s x /\ x < d))
    (right_bst : bst tr (fun x => s x /\ x > d))
    (d_elem : s d),
    bst (Node tl d tr) s.

This inductive definition is equivalent to the one given in the lab, but is nicer to handle, as the generated induction principle gives us the shape of the tree "for free". For example:

Lemma bst_iff : forall tr P Q,
    bst tr P ->
    (forall x, P x <-> Q x) ->
    bst tr Q.
forall (tr : tree) (P Q : nat -> Prop),
bst tr P -> (forall x : nat, P x <-> Q x) -> bst tr Q
Proof.
forall (tr : tree) (P Q : nat -> Prop),
bst tr P -> (forall x : nat, P x <-> Q x) -> bst tr Q
  intros tr P Q Hbst.
tr: tree
P, Q: nat -> Prop
Hbst: bst tr P
(forall x : nat, P x <-> Q x) -> bst tr Q
  revert Q. (* We need a stronger induction hypothesis. *)
tr: tree
P: nat -> Prop
Hbst: bst tr P
forall Q : nat -> Prop,
(forall x : nat, P x <-> Q x) -> bst tr Q
  (* We induct on bst instead of tr! *)
  induction Hbst; intros.
s: nat -> Prop
s_empty: forall x : nat, ~ s x
Q: nat -> Prop
H: forall x : nat, s x <-> Q x
bst Leaf Q
s: nat -> Prop
tl: tree
d: nat
tr: tree
Hbst1: bst tl (fun x : nat => s x /\ x < d)
Hbst2: bst tr (fun x : nat => s x /\ x > d)
d_elem: s d
IHHbst1: forall Q : nat -> Prop,
(forall x : nat, s x /\ x < d <-> Q x) -> bst tl Q
IHHbst2: forall Q : nat -> Prop,
(forall x : nat, s x /\ x > d <-> Q x) -> bst tr Q
Q: nat -> Prop
H: forall x : nat, s x <-> Q x
bst (Node tl d tr) Q
  -
s: nat -> Prop
s_empty: forall x : nat, ~ s x
Q: nat -> Prop
H: forall x : nat, s x <-> Q x
bst Leaf Q constructor.
s: nat -> Prop
s_empty: forall x : nat, ~ s x
Q: nat -> Prop
H: forall x : nat, s x <-> Q x
forall x : nat, ~ Q x firstorder.
  -
s: nat -> Prop
tl: tree
d: nat
tr: tree
Hbst1: bst tl (fun x : nat => s x /\ x < d)
Hbst2: bst tr (fun x : nat => s x /\ x > d)
d_elem: s d
IHHbst1: forall Q : nat -> Prop,
(forall x : nat, s x /\ x < d <-> Q x) -> bst tl Q
IHHbst2: forall Q : nat -> Prop,
(forall x : nat, s x /\ x > d <-> Q x) -> bst tr Q
Q: nat -> Prop
H: forall x : nat, s x <-> Q x
bst (Node tl d tr) Q
    constructor; firstorder.
Qed.

Using lemmas about compose

Some of you might have noticed that attempting to use rewrite on the ~= relation will not work out of the box. The reason for that is that rewrite does not rewrite under binders:

Lemma compose_left_congruence {A B C: Type} :
  forall (f g: A -> B) (h: B -> C),
  f ~= g ->
  h ∘ f ~= h ∘ g.
A, B, C: Type
forall (f g : A -> B) (h : B -> C),
f ~= g -> h ∘ f ~= h ∘ g
Proof.
A, B, C: Type
forall (f g : A -> B) (h : B -> C),
f ~= g -> h ∘ f ~= h ∘ g
  intros.
A, B, C: Type
f, g: A -> B
h: B -> C
H: f ~= g
h ∘ f ~= h ∘ g
  unfold "∘".
A, B, C: Type
f, g: A -> B
h: B -> C
H: f ~= g
(fun x : A => h (f x)) ~= (fun x : A => h (g x))
  rewrite H.
Found no subterm matching "f ?M1581"
in the current goal.
A, B, C: Type
f, g: A -> B
h: B -> C
H: f ~= g
(fun x : A => h (f x)) ~= (fun x : A => h (g x))

Instead, one first has to remove the (hidden) quantifier in ~= before proceeding:

  intro x.
A, B, C: Type
f, g: A -> B
h: B -> C
H: f ~= g
x: A
h (f x) = h (g x)
  rewrite H.
A, B, C: Type
f, g: A -> B
h: B -> C
H: f ~= g
x: A
h (g x) = h (g x)
  reflexivity.
Qed.

Backward vs forward reasoning

There exists two styles in which one can do proofs in Rocq:

• The forward style is the traditional mathematical style, where to prove that P -> Q one sequentially proves that P -> P1, P1 -> P2, and so on, until finally Q is reached.

• The backward style is the opposite: to prove P -> Q, one derives sufficient assumptions in which Q holds, and progressively reduces those assumptions until P is reached.

Each style has its own trade-offs: the forward style is more natural to mathematicians (i.e. closer to textbook practice), but leads to more verbose proof scripts; on the other hand, the backward style tends to produce shorter (but less readable) proofs, but is more amenable to proof search.

Rocq favors the backward style for its conciseness, and most tactics you'll see work in this style. For example, the backward-style replace tactic generates an equality subgoal for each replacement made:

Goal forall n, (n + 1) / ((n + 1 - 0) * (1 ^ 2)) = 1.
forall n : nat, (n + 1) / ((n + 1 - 0) * 1 ^ 2) = 1
Proof.
forall n : nat, (n + 1) / ((n + 1 - 0) * 1 ^ 2) = 1
  intros.
n: nat
(n + 1) / ((n + 1 - 0) * 1 ^ 2) = 1
  replace (1 ^ 2) with 1 by reflexivity.
n: nat
(n + 1) / ((n + 1 - 0) * 1) = 1
  replace (n + 1 - 0) with (n + 1) by lia.
n: nat
(n + 1) / ((n + 1) * 1) = 1
  replace ((n + 1) * 1) with (n + 1) by lia.
n: nat
(n + 1) / (n + 1) = 1
  apply Nat.div_same; lia.
Qed.

…which, in forward-style, is equivalent to the following proof that uses assert and rewrite instead:

Goal forall n, (n + 1) / ((n + 1 - 0) * (1 ^ 2)) = 1.
forall n : nat, (n + 1) / ((n + 1 - 0) * 1 ^ 2) = 1
Proof.
forall n : nat, (n + 1) / ((n + 1 - 0) * 1 ^ 2) = 1
  intros.
n: nat
(n + 1) / ((n + 1 - 0) * 1 ^ 2) = 1

  assert (1 ^ 2 = 1).
n: nat
1 ^ 2 = 1
n: nat
H: 1 ^ 2 = 1
(n + 1) / ((n + 1 - 0) * 1 ^ 2) = 1 {
n: nat
1 ^ 2 = 1
    simpl.
n: nat
1 = 1
    reflexivity.
  }
n: nat
H: 1 ^ 2 = 1
(n + 1) / ((n + 1 - 0) * 1 ^ 2) = 1
  rewrite H.
n: nat
H: 1 ^ 2 = 1
(n + 1) / ((n + 1 - 0) * 1) = 1

  assert (n + 1 - 0 = n + 1) as H0 by lia.
n: nat
H: 1 ^ 2 = 1
H0: n + 1 - 0 = n + 1
(n + 1) / ((n + 1 - 0) * 1) = 1
  rewrite H0.
n: nat
H: 1 ^ 2 = 1
H0: n + 1 - 0 = n + 1
(n + 1) / ((n + 1) * 1) = 1

  assert ((n + 1) * 1 = (n + 1)) as H1 by lia.
n: nat
H: 1 ^ 2 = 1
H0: n + 1 - 0 = n + 1
H1: (n + 1) * 1 = n + 1
(n + 1) / ((n + 1) * 1) = 1
  rewrite H1.
n: nat
H: 1 ^ 2 = 1
H0: n + 1 - 0 = n + 1
H1: (n + 1) * 1 = n + 1
(n + 1) / (n + 1) = 1

  rewrite Nat.div_same.
n: nat
H: 1 ^ 2 = 1
H0: n + 1 - 0 = n + 1
H1: (n + 1) * 1 = n + 1
1 = 1
n: nat
H: 1 ^ 2 = 1
H0: n + 1 - 0 = n + 1
H1: (n + 1) * 1 = n + 1
n + 1 <> 0
  reflexivity.
n: nat
H: 1 ^ 2 = 1
H0: n + 1 - 0 = n + 1
H1: (n + 1) * 1 = n + 1
n + 1 <> 0

  lia.
Qed.

In most cases, we'll prefer the first proof, which is much easier to review.

Destructive tactics

Some tactics that manipulate the context can have a destructive behavior, leading to unprovable goals. For example, induct forgets about the term it is inducting on if it's not a variable:

Inductive even : nat -> Prop :=
| Even0 : even 0
| EvenSS : forall n, even n -> even (S (S n)).

Theorem even_SS : forall n,
    even (S (S n)) -> even n.
forall n : nat, even (S (S n)) -> even n
Proof.
forall n : nat, even (S (S n)) -> even n
  intros.
n: nat
H: even (S (S n))
even n
  induction H.
n: nat
even n
n, n0: nat
H: even n0
IHeven: even n
even n
  (* Stuck! *)
Abort.

To work-around that, one can use the remember tactics, which explicitly introduces an equality hypothesis:

Theorem even_SS : forall n,
    even (S (S n)) -> even n.
forall n : nat, even (S (S n)) -> even n
Proof.
forall n : nat, even (S (S n)) -> even n
  intros.
n: nat
H: even (S (S n))
even n
  remember (S (S n)) as n'.
n, n': nat
Heqn': n' = S (S n)
H: even n'
even n
  induction H.
n: nat
Heqn': 0 = S (S n)
even n
n, n0: nat
Heqn': S (S n0) = S (S n)
H: even n0
IHeven: n0 = S (S n) -> even n
even n
  -
n: nat
Heqn': 0 = S (S n)
even n discriminate.
  -
n, n0: nat
Heqn': S (S n0) = S (S n)
H: even n0
IHeven: n0 = S (S n) -> even n
even n injection Heqn' as ?.
n, n0: nat
H0: n0 = n
H: even n0
IHeven: n0 = S (S n) -> even n
even n
    subst.
n: nat
IHeven: n = S (S n) -> even n
H: even n
even n
    assumption.
Qed.

Some other examples of destructive tactics include destruct, specialize, subst, and clear.