The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Tue, 9 Oct 2012 02:25:46 -0700,
dan portin 
<danportin AT gmail.com>
 a écrit :

> In order to understand how to write functions with dependent pattern
> matching, I decided to write a library of dependently typed AVL trees
> mirroring the implementation of AVL trees in the Agda standard
> library. The binary search tree property is enforced as usual, by
> encoding lower and upper bounds on tree elements as type parameters.
> The balancing property for AVL trees is encoded by indexing the trees
> by their height, and ensuring that the absolute value of the
> difference between the heights never exceeds one via the constructors
> for Bal. Here is an example with the type of the tree elements
> (parameterized over a computable linear order with setoid equality)
> specialized to naturals, so as to be relatively brief:
> 
> Require Import Unicode.Utf8.
> Require Import Utf8_core.
> Require Import Arith.
> 
> Inductive Bal : nat → nat → Set :=
>   | E : ∀ {h : nat}, Bal h h
>   | P : ∀ {h : nat}, Bal h (S h)
>   | N : ∀ {h : nat}, Bal (S h) h.
> 
> Definition maxB {n m : nat} (φ : Bal n m) : nat :=
>   match φ with
>     | E h => h
>     | P h => S h
>     | N h => S h
>   end.
> 
> Inductive T (ρ₁ ρ₂ : nat) : nat → Type :=
>     | Leaf : ρ₁ < ρ₂ → T ρ₁ ρ₂ 0
>     | Node : ∀ {h₁ h₂} (φ : Bal h₁ h₂) (x : nat), T ρ₁ x h₁ → T x ρ₂
> h₂ → T ρ₁ ρ₂ (S (maxB φ)).
> 
> Arguments Leaf [ρ₁ ρ₂] H.
> Arguments Node [ρ₁ ρ₂ h₁ h₂] φ x l r.
> 
> One of the functions necessary for defining insert joins two AVL
> trees and one element, where the height of the first AVL tree may
> violate the balancing invariant by one. This is encoded using a
> dependent pair of an element of a two-element type along with an AVL
> tree. I have used bool for the two-element type, although it would
> probably be better to define a custom datatype for bits:
> 
> Definition succB (i : bool) (n : nat) :=
>   match i with
>     | true  => S n
>     | false => n
>   end.
> 
> Definition joinL₁ {ρ₁ ρ₂ h₁ h₂} (φ₁ : Bal h₁ h₂) (x₁ : nat)
>   (σ : {i : bool & T ρ₁ x₁ (succB i h₁)}) (t₂ : T x₁ ρ₂ h₂) :
>     {i : bool & T ρ₁ ρ₂ (succB i (S (maxB φ₁)))} := ...
> 
> There are several lemmas necessary to write joinL₁, so I will list
> them and then the definition of joinL₁ essentially translated from
> Agda. The definition of the latter may not be the prettiest, and uses
> the "convoy pattern" trick from Chlipala's book in order to generate
> elements of my data structure with the correct types. I could
> probably afford to generate some abstractions that would improve
> readability. See the Agda stlib for a specification:
> 
> Definition injS {x y : nat} : S x = S y → x = y :=
>   λ H : S x = S y, f_equal pred H.
> 
> Definition unjS {x y : nat} : x = y → S x = S y :=
>   λ H : x = y, f_equal S H.
> 
> Definition caseS (n : nat) (A : Type) : Type :=
>   nat_rect (λ x, Type) unit (λ x y, A) n.
> 
> Notation "'rewL' E 'in' H" := (eq_rect _ _ H _ E) (at level 10, H at
> level 10).
> Notation "'rewR' E 'in' H" := (eq_rect_r _ H E)   (at level 10, H at
> level 10).
> 
> Lemma balS {n m : nat} : Bal n m → Bal (S n) (S m).
> Proof. destruct 1; constructor. Defined.
> 
> Lemma maxR {n m : nat} (φ : Bal n m) : Bal (maxB φ) n.
> Proof. destruct φ; constructor. Defined.
> 
> Lemma maxL {n m : nat} (φ : Bal n m) : Bal m (maxB φ).
> Proof. destruct φ; constructor. Defined.
> 
> Lemma maxS {n m : nat} (φ : Bal n m) : Bal (maxB (maxR φ)) (maxB
> (maxL φ)). Proof. destruct φ; constructor. Defined.
> 
> Lemma maxB_lemma {n m : nat} (φ : Bal n m) : S (maxB (balS (maxS φ)))
> = S (S (maxB φ)).
> Proof. destruct φ; reflexivity. Defined.
> 
> Lemma succtrue {n : nat} : succB true n = S n.
> Proof. auto. Defined.
> 
> Lemma succfalse {n : nat} : succB false n = n.
> Proof. auto. Defined.
> 
> Definition joinL₁ {ρ₁ ρ₂ h₁ h₂} (φ₁ : Bal h₁ h₂) (x₁ : nat)
>   (σ : {i : bool & T ρ₁ x₁ (succB i h₁)}) (t₂ : T x₁ ρ₂ h₂) :
>     {i : bool & T ρ₁ ρ₂ (succB i (S (maxB φ₁)))} :=
>   match (projT1 σ) as i₁ return
>   T ρ₁ x₁ (succB i₁ h₁) → {i : bool & T ρ₁ ρ₂ (succB i (S (maxB
> φ₁)))} with | false => λ (t₁ : T ρ₁ x₁ (succB false h₁)),
>       existT (λ i : bool, T ρ₁ ρ₂ (succB i (S (maxB φ₁)))) false
> (Node φ₁ x₁ t₁ t₂)
>     | true => λ (t₁ : T ρ₁ x₁ (succB true h₁)),
>       match φ₁ as φ₁ in Bal h₁ h₂ return
>       T ρ₁ x₁ (succB true h₁) → T x₁ ρ₂ h₂ →
>       {i : bool & T ρ₁ ρ₂ (succB i (S (maxB φ₁)))} with
>         | E η₁ => λ (t₁ : T ρ₁ x₁ (succB true η₁)) (t₂ : T x₁ ρ₂ η₁),
>           existT (λ i : bool, T ρ₁ ρ₂ (succB i (S (maxB E)))) true
> (Node N x₁ t₁ t₂)
>         | P η₁ => λ (t₁ : T ρ₁ x₁ (succB true η₁)) (t₂ : T x₁ ρ₂ (S
> η₁)), existT (λ i : bool, T ρ₁ ρ₂ (succB i (S (maxB P)))) false (Node
> E x₁ t₁ t₂)
>         | N η₁ => λ (t₁ : T ρ₁ x₁ (succB true (S η₁))) (t₂ : T x₁ ρ₂
> η₁), match t₁ in T _ _ η return
>           η = succB true (S η₁) → caseS η {i : bool & T ρ₁ ρ₂ (succB
> i (S (maxB N)))} with
>             | Leaf _ => λ (E₁ : O = succB true (S η₁)), tt
>             | Node h₃ h₄ φ₂ x₂ t₃ t₄ => λ (E₁ : S (maxB φ₂) = succB
> true (S η₁)),
>               match φ₂ as φ₂ in Bal h₃ h₄ return
>               T ρ₁ x₂ h₃ → T x₂ x₁ h₄ → maxB φ₂ = S η₁ →
>               {i : bool & T ρ₁ ρ₂ (succB i (S (maxB N)))} with
>                 | E η₂ => λ (t₃ : T ρ₁ x₂ η₂) (t₄ : T x₂ x₁ η₂) (E₂ :
> maxB E = S η₁),
>                   let τ₁ := Node N x₁ (rewL E₂ in t₄) t₂ in
>                   existT (λ i : bool, T ρ₁ ρ₂ (succB i (S (maxB N))))
> true (Node P x₂ (rewL E₂ in t₃) τ₁)
>                 | N η₂ => λ (t₃ : T ρ₁ x₂ (S η₂)) (t₄ : T x₂ x₁ η₂)
> (E₂ : maxB N = S η₁),
>                   let τ₁ := Node E x₁ (rewL (injS E₂) in t₄) t₂ in
>                   existT (λ i : bool, T ρ₁ ρ₂ (succB i (S (maxB N))))
> false (Node E x₂ (rewL E₂ in t₃) τ₁)
>                 | P η₂ => λ (t₃ : T ρ₁ x₂ η₂) (t₄ : T x₂ x₁ (S η₂))
> (E₂ : maxB P = S η₁),
>                   match t₄ in T _ _ η return
>                   η = S η₂ → caseS η {i : bool & T ρ₁ ρ₂ (succB i (S
> (maxB N)))} with
>                     | Leaf _ => λ E₃ : 0 = S η₂, tt
>                     | Node h₅ h₆ φ₃ x₃ t₅ t₆ => λ E₃ : S (maxB φ₃) =
> S η₂, let τ₁ := Node (maxR φ₃) x₂ (rewR (injS E₃) in t₃)
> t₅              in
>                       let τ₂ := Node (maxL φ₃) x₁ t₆ (rewR (injS
> (rewL E₂ in E₃)) in t₂) in
>                       let τ₃ := rewL (maxB_lemma φ₃) in Node (balS
> (maxS φ₃)) x₃ τ₁ τ₂   in
>                       let τ₄ := rewR succfalse in (rewL (unjS (rewL
> E₂ in E₃)) in τ₃)     in
>                       existT (λ i : bool, T ρ₁ ρ₂ (succB i (S (maxB
> N)))) false τ₄
>                   end eq_refl
>               end t₃ t₄ (injS E₁)
>           end eq_refl
>       end t₁ t₂
>   end (projT2 σ).
> 
> I am having the following problem. Consider the membership function
> over AVL trees and the following lemma, which states that joinL₁
> preserves tree membership. This is necessary in order to prove that,
> for instance, the insertion function behaves correctly with respect
> to set membership for a library of finite sets:
> 
> Fixpoint mem {ρ₁ ρ₂ h} (x : nat) (t : T ρ₁ ρ₂ h) : Prop :=
>       match t with
>         | Leaf H             => False
>         | Node h₁ h₂ φ y l r =>
>           match lt_eq_lt_dec x y with
>             | inleft (right EQ) => True
>             | inleft (left  LT) => mem x l
>             | inright       GT  => mem x r
>           end
>       end.
> 
> Definition mem_joinL₁ {ρ₁ ρ₂ h₁ h₂} (φ₁ : Bal h₁ h₂) (x₁ : nat)
>   (σ : {i : bool & T ρ₁ x₁ (succB i h₁)}) (t₂ : T x₁ ρ₂ h₂) :
>     ∀ y : nat, mem y (projT2 (joinL₁ φ₁ x₁ σ t₂)) ↔
>                mem y (projT2 σ) ∨ mem y t₂ ∨ x₁ = y.
> Proof.
>   destruct σ as [i₁ t₁].
>   destruct i₁.
>     destruct φ₁.
>     admit.
>     admit.
>     dependent destruction t₁.
>     dependent destruction φ.
>       admit.
>       admit.
>       admit.
>   admit.
> Qed.
> 
> With the knowledge that lt is irreflexive and asymmetric, along with
> some simple tactics, it's trivial to prove the first two and last
> holes in the proof of mem_joinL₁.  The problem comes in the third,
> fourth, and fifth holes. What happens is that Coq refuses to simplify
> joinL₁ because dependent destruction is not destructing t₁ correctly.
> For instance,
> 
>   ρ₁ : nat
>   ρ₂ : nat
>   h : nat
>   x₁ : nat
>   h0 : nat
>   x0 : nat
>   t₁1 : T ρ₁ x0 h0
>   t₁2 : T x0 x₁ h0
>   t₁0 : T ρ₁ x₁ (succB true (S h))
>   x1 : maxB E = S h
>   x : Node E x0 t₁1 t₁2 ~= t₁0
>   t₂ : T x₁ ρ₂ h
>   ============================
>    ∀ y : nat,
>    mem y
>      (projT2
>         (joinL₁ N x₁ (existT (λ i : bool, T ρ₁ x₁ (succB i (S h)))
> true t₁0) t₂))
>    ↔ mem y (projT2 (existT (λ i : bool, T ρ₁ x₁ (succB i (S h))) true
> t₁0)) ∨ mem y t₂ ∨ x₁ = y
> 
> The second instance of existT _ true t₁0 simplifies as expected, but
> the first instance does not. I assume that the problem has to do with
> a conflict between the types that joinL₁ and the dependent pair
> expect. However, I cannot figure out how to rewrite using x1 and x in
> combination with generalizations of variables, pattern, and so forth,
> in order to generate a term which will simplify appropriately. The
> solution that I am working on is to write the proof term by hand,
> using elimination predicates in order to generate terms with the
> correct types. This doesn't seem like the best solution. Is there one?

I would suggest you to put the depth as a parameter instead of an
indice in your T type.

(You can try to redefine my joinL₁ without tactics, you just have to do
a Print joinL₁, copy paste the output, indent, add lacking anotations,
remove useless ones)

===============================

Require Import Unicode.Utf8.
Require Import Utf8_core.
Require Import Arith.

Inductive Bal : nat → nat → Set :=
  | E : ∀ {h : nat}, Bal h h
  | P : ∀ {h : nat}, Bal h (S h)
  | N : ∀ {h : nat}, Bal (S h) h.

Definition maxB {n m : nat} (φ : Bal n m) : nat :=
  match φ with
    | E h => h
    | P h => S h
    | N h => S h
  end.

Inductive T (ρ₁ ρ₂ h : nat) : Type :=
    | Leaf : h = 0 → ρ₁ < ρ₂ → T ρ₁ ρ₂ h
    | Node : ∀ {h₁ h₂} (φ : Bal h₁ h₂) (x : nat),
             h = S (maxB φ) → T ρ₁ x h₁ → T x ρ₂ h₂ →
             T ρ₁ ρ₂ h.

Arguments Leaf [ρ₁ ρ₂] h Heq H.
Arguments Node [ρ₁ ρ₂] h [h₁ h₂] φ x Heq l r.

Definition succB (i : bool) (n : nat) :=
  match i with
    | true  => S n
    | false => n
  end.

Definition injS {x y : nat} : S x = S y → x = y :=
  λ H : S x = S y, f_equal pred H.

Definition unjS {x y : nat} : x = y → S x = S y :=
  λ H : x = y, f_equal S H.

Definition caseS (n : nat) (A : Type) : Type :=
  nat_rect (λ x, Type) unit (λ x y, A) n.

Notation "'rewL' E 'in' H" := (eq_rect _ _ H _ E) (at level 10, H at
level 10).
Notation "'rewR' E 'in' H" := (eq_rect_r _ H E)   (at level 10, H at
level 10).

Lemma balS {n m : nat} : Bal n m → Bal (S n) (S m).
Proof. destruct 1; constructor. Defined.

Lemma maxR {n m : nat} (φ : Bal n m) : Bal (maxB φ) n.
Proof. destruct φ; constructor. Defined.

Lemma maxL {n m : nat} (φ : Bal n m) : Bal m (maxB φ).
Proof. destruct φ; constructor. Defined.

Lemma maxS {n m : nat} (φ : Bal n m) : Bal (maxB (maxR φ)) (maxB (maxL
φ)). Proof. destruct φ; constructor. Defined.

Lemma maxB_lemma {n m : nat} (φ : Bal n m) : maxB (balS (maxS φ)) = S
(maxB φ). Proof. destruct φ; reflexivity. Defined.

Lemma succtrue {n : nat} : succB true n = S n.
Proof. auto. Defined.

Lemma succfalse {n : nat} : succB false n = n.
Proof. auto. Defined.

Definition joinL₁ {ρ₁ ρ₂ h₁ h₂} (φ₁ : Bal h₁ h₂) (x₁ : nat)
  (σ : {i : bool & T ρ₁ x₁ (succB i h₁)}) (t₂ : T x₁ ρ₂ h₂) :
    {i : bool & T ρ₁ ρ₂ (succB i (S (maxB φ₁)))}.

generalize (projT2 σ).
destruct (projT1 σ); simpl; clear σ.

destruct φ₁.
exists true.
right with (S h) h N x₁; auto.
exists false.
right with (S h) (S h) E x₁; auto.
intros [Heq H|h₁ h₂ φ₂ x₂ Heq l r].
refine (match Heq with eq_refl => I end).
generalize (injS Heq); clear Heq.
destruct φ₂; simpl in *; intros.
exists true.
simpl in *.
right with h0 (S h0) P x₂; simpl; auto.
right with (S h) h N x₁; simpl; auto.
revert r; destruct H; auto.

destruct r.
generalize I.
refine (match e with eq_refl => I end).
exists false.

right with _ _ (balS (maxS φ)) x; simpl; auto.
revert e H.
destruct (maxB_lemma φ).
intros [].
intros [].
split.
right with _ _ (maxR φ) x₂; simpl; auto.
case (injS e); auto.
right with _ _ (maxL φ) x₁; simpl; auto.
case (injS e); auto.
case (injS H); auto.

exists false.
right with (S h0) (S h0) E x₂; simpl; auto.
right with h h E x₁; simpl; auto.
revert r.
generalize (injS H).
intros []; auto.

exists false; simpl.
right with h₁ h₂ φ₁ x₁; auto.
Defined.

Fixpoint mem {ρ₁ ρ₂ h} (x : nat) (t : T ρ₁ ρ₂ h) : Prop :=
      match t with
        | Leaf _ H           => False
        | Node h₁ h₂ φ y H l r =>
          match lt_eq_lt_dec x y with
            | inleft (right EQ) => True
            | inleft (left  LT) => mem x l
            | inright       GT  => mem x r
          end
      end.

Definition mem_joinL₁ {ρ₁ ρ₂ h₁ h₂} (φ₁ : Bal h₁ h₂) (x₁ : nat)
  (σ : {i : bool & T ρ₁ x₁ (succB i h₁)}) (t₂ : T x₁ ρ₂ h₂) :
    ∀ y : nat, mem y (projT2 (joinL₁ φ₁ x₁ σ t₂)) ↔
               mem y (projT2 σ) ∨ mem y t₂ ∨ x₁ = y.
Proof.
  destruct σ as [i₁ t₁].
  destruct i₁.
    destruct φ₁.