text:
(** * The original, non-extensional binary tries *)

(* Authors: Xavier Leroy and Damien Doligez, Inria.
   Copyright: Inria.
   License: BSD-3-Clause. *)

(** This implementation of binary tries is taken from the Maps module
    of CompCert version 3.9,
    https://compcert.org/doc-3.9/html/compcert.lib.Maps.html
    Several operations were omitted, and some proofs were tightened.
*)

From Coq Require Import PArith.

Set Implicit Arguments.

Module PTree.

(** ** Representation of tries *)

Inductive tree (A: Type) : Type :=
  | Leaf: tree A
  | Node: tree A -> option A -> tree A -> tree A.

Arguments Leaf {A}.
Arguments Node [A].

Definition t := tree.

(** A smart constructor that avoids creating nodes that contain no data. *)

Definition Node' {A} (l: tree A) (x: option A) (r: tree A): tree A :=
  match l, x, r with
  | Leaf, None, Leaf => Leaf
  | _, _, _ => Node l x r
  end.

(** ** Basic operations: [empty], [get], [set], [remove] *)

Definition empty (A: Type) : tree A := Leaf.

Fixpoint get (A: Type) (i: positive) (m: tree A) {struct m} : option A :=
  match m with
  | Leaf => None
  | Node l o r =>
      match i with
      | xH => o
      | xO ii => get ii l
      | xI ii => get ii r
      end
  end.

Fixpoint set (A: Type) (i: positive) (v: A) (m: tree A) {struct i} : tree A :=
  match m with
  | Leaf =>
      match i with
      | xH => Node Leaf (Some v) Leaf
      | xO ii => Node (set ii v Leaf) None Leaf
      | xI ii => Node Leaf None (set ii v Leaf)
      end
  | Node l o r =>
      match i with
      | xH => Node l (Some v) r
      | xO ii => Node (set ii v l) o r
      | xI ii => Node l o (set ii v r)
      end
  end.

Fixpoint remove (A: Type) (i: positive) (m: tree A) {struct m} : tree A :=
  match m with
  | Leaf => Leaf
  | Node l o r =>
      match i with
      | xH => Node' l None r
      | xO ii => Node' (remove ii l) o r
      | xI ii => Node' l o (remove ii r)
      end
  end.

(** ** Good variable properties for the basic operations *)

(** The following equations specify the [empty], [set] and [remove]
    operations in terms of [get] queries.  For example,
    [gempty] characterizes [empty] as the trie that always responds
    "not found" to a [get]. *)

Theorem gempty:
  forall {A} (i: positive), get i (empty A) = None.
Proof.
  auto.
Qed.

Theorem gss:
  forall {A} (i: positive) (x: A) (m: tree A), get i (set i x m) = Some x.
Proof.
  induction i; destruct m; simpl; auto.
Qed.

Theorem gso:
  forall {A} (i j: positive) (x: A) (m: tree A),
  i <> j -> get i (set j x m) = get i m.
Proof.
  induction i; intros; destruct j; destruct m; simpl; auto; try apply IHi; congruence.
Qed.

Lemma gNode':
  forall {A} (i: positive) (l: tree A) (x: option A) (r: tree A),
  get i (Node' l x r) = match i with xH => x | xO j => get j l | xI j => get j r end.
Proof.
  intros. destruct l, x, r; simpl; auto. destruct i; auto.
Qed.

Theorem grs:
  forall {A} (i: positive) (m: tree A), get i (remove i m) = None.
Proof.
  induction i; destruct m; simpl; auto; rewrite gNode'; simpl; auto.
Qed.

Theorem gro:
  forall {A} (i j: positive) (m: tree A),
  i <> j -> get i (remove j m) = get i m.
Proof.
  induction i; destruct j, m; intros; simpl; auto;
  rewrite gNode'; simpl; auto; try apply IHi; congruence.
Qed.

(** ** Collective operations over tries *)

(** The [map_filter] operation combines a "map" (apply a function to
    every value of a trie) and a "filter" (keep only the values
    that satisy a given predicate).  The function [f] being mapped
    has type [A -> option B].  A value [a] in the input trie
    becomes a value [b] in the output trie if [f a = Some b]
    and is absent in the output trie if [f a = None]. *)

Section MAP_FILTER.

Variables A B: Type.

Definition option_map (f: A -> option B) (o: option A): option B :=
  match o with None => None | Some a => f a end.

Fixpoint map_filter (f: A -> option B) (m: tree A) : tree B :=
  match m with
  | Leaf => Leaf
  | Node l o r => Node' (map_filter f l) (option_map f o) (map_filter f r)
  end.

Lemma gmap_filter:
  forall (f: A -> option B) (m: tree A) (i: positive),
  get i (map_filter f m) = option_map f (get i m).
Proof.
  induction m; intros; simpl.
  - auto.
  - rewrite gNode'. destruct i; auto.
Qed.

End MAP_FILTER.

(** The [combine] operation traverses two tries in parallel,
    applying a function [f: option A -> option B -> option C]
    at each node to build the resulting trie. *)

Section COMBINE.

Variables A B C: Type.
Variable f: option A -> option B -> option C.
Hypothesis f_None_None: f None None = None.

Fixpoint combine (m1: tree A) (m2: tree B): tree C :=
  match m1, m2 with
  | Leaf, _ => map_filter (fun b => f None (Some b)) m2
  | _, Leaf => map_filter (fun a => f (Some a) None) m1
  | Node l1 o1 r1, Node l2 o2 r2 => Node' (combine l1 l2) (f o1 o2) (combine r1 r2)
  end.

Lemma gcombine:
  forall (m1: tree A) (m2: tree B) (i: positive),
  get i (combine m1 m2) = f (get i m1) (get i m2).
Proof.
  Local Opaque map_filter.
  induction m1; intros.
- simpl. rewrite gmap_filter. destruct (get i m2); auto.
- destruct m2; simpl combine.
  + rewrite gmap_filter. destruct (get i (Node m1_1 o m1_2)); auto.
  + rewrite gNode'; simpl. destruct i; auto.
Qed.

End COMBINE.

End PTree.

author: xavierleroy

repo: canonical-binary-tries


text:
Require Import SpecDeps.
Require Import RData.
Require Import EventReplay.
Require Import MoverTypes.
Require Import Constants.
Require Import CommonLib.
Require Import AbsAccessor.Spec.

Local Open Scope Z_scope.

Section SpecLow.

  Fixpoint table_maps_block_loop0 n i ret table base_pa level ipa_state adt :=
    match n with
    | O => Some (i, ret)
    | S n' =>
      match table_maps_block_loop0 n' i ret table base_pa level ipa_state adt with
      | Some (i, ret) =>
        rely is_int i; rely is_int ret;
        when' pgte == pgte_read_spec table (VZ64 i) adt;
        rely is_int64 pgte;
        let expected_pa := base_pa + i * GRANULE_SIZE in
        rely is_int64 expected_pa;
        if PTE_TO_IPA_STATE pgte =? ipa_state then
          when' phys == entry_to_phys_spec (VZ64 pgte) (VZ64 level) adt;
          rely is_int64 phys;
          if phys =? expected_pa then
            Some (i + 1, ret)
          else
            Some (i + 1, 0)
        else Some (i + 1, 0)
      | _ => None
      end
    end.

  Definition table_maps_block_spec0 (table: Pointer) (level: Z64) (ipa_state: Z64) (adt: RData) : option Z :=
    match level, ipa_state with
    | VZ64 level, VZ64 ipa_state =>
      rely is_int64 level; rely is_int64 ipa_state;
      when' pgte == pgte_read_spec table (VZ64 0) adt;
      rely is_int64 pgte;
      when' base_pa == entry_to_phys_spec (VZ64 pgte) (VZ64 level) adt;
      rely is_int64 base_pa; rely is_int64 (level - 1);
      when aligned == addr_is_level_aligned_spec (VZ64 base_pa) (VZ64 (level - 1)) adt;
      rely is_int aligned;
      if aligned =? 0 then Some 0 else
        match table_maps_block_loop0 (Z.to_nat PGTES_PER_TABLE) 0 1 table base_pa level ipa_state adt with
        | Some (i, ret) =>
          rely is_int i; rely is_int ret;
          Some ret
        | _ => None
        end
    end.

End SpecLow.

author: columbia


text:
Definition plus_comm := forall n m : nat, n + m = m + n.

Theorem plus_comm_proof: plus_comm.
Proof.
  unfold plus_comm.
  induction n.
  - simpl.
    SearchRewrite (_ + _).
    intros.
    rewrite <- plus_n_O.
    reflexivity.
  - simpl.
    intros.
    SearchRewrite (_ + _).
    rewrite IHn.
    rewrite plus_n_Sm.
    reflexivity.
Qed.

author: minaminao

repo: proof-assistant-contest


text:
Require Import List.

(** We need a type for the lambda variables.
    This type should be infinite and the equality should be decidable.
    We make the decidability of the equality an hypothesis.
    The other possibility would have been to create an infinite ad hoc
    type with a decidable equality. This second option would have
    necessitate type constructors and a proof of the decidability of the
    equality.
*)
Variable A : Type.

Hypothesis A_eq_dec: forall x y: A, {x = y} + {x <> y}.

(** **Type declaration** *)
(** An untyped lambda term is either:
    - a variable from a given Set
    - the abstraction of a variable from a Term
    - the application of a Term to another one.
 *)
Inductive term : Type :=
| var : A -> term
| abs : A -> term -> term
| app : term -> term -> term.

(** **Some functions about terms** *)

(**
We will need a type for the set of variables. There are two sort of possibilities
here:
1. Implement a lightweight type of my own.
2. Use a type from the Coq standard library (e.g. ListSet)
*)

(** My own declaration and lightweight implementation of var_set *)
Definition var_set := list A.

Definition empty_var_set : var_set := nil.

Fixpoint add_var_set (a:A) (s:var_set) : var_set :=
  match s with
  | nil => a::nil
  | h::t =>
    match A_eq_dec a h with
    | left _ => h::t
    | right _ => h::add_var_set a t
    end
  end.

Fixpoint remove_var_set (a:A) (s:var_set) : var_set :=
  match s with
  | nil => nil
  | h::t =>
    match A_eq_dec a h with
    | left _ => t
    | right _ => remove_var_set a t
    end
  end.

Fixpoint in_var_set (a:A) (s:var_set) : bool :=
  match s with
  | nil => false
  | h::t =>
    match A_eq_dec a h with
    | left _ => true
    | right _ => in_var_set a t
    end
  end.

Fixpoint union_var_set (s1:var_set) (s2:var_set) : var_set :=
  match s1 with
  | nil => s2
  | h::t => add_var_set h (union_var_set t s2)
  end.

Fixpoint inter_var_set (s1 s2: var_set) : var_set :=
  match s1 with
  | nil => nil
  | h::t => if in_var_set h s2
           then add_var_set h (inter_var_set t s2)
           else inter_var_set t s2
  end.

Fixpoint minus_var_set (s1 s2: var_set) : var_set :=
  match s2 with
  | nil => s1
  | h::t => if in_var_set h s1
           then minus_var_set (remove_var_set h s1) t
           else minus_var_set s1 t
  end.

(** The ListSet library defines a Predicate set_In
 This definition relies on the In Predicate for the Lists:

 Fixpoint In (a:A) (l:list A) : Prop:=
   match l with
     | [] => False
     | b :: m => b = a \/ In a m
   end.

 *)
Definition var_set_In : A -> var_set -> Prop := In (A:=A).

(** an element is in the var_set it was just add to.
    The proof is more complicated than for simple lists
    as there is an equality test in the add_var_set function.
*)
Theorem in_eq : forall (a:A) (s:var_set), var_set_In a (add_var_set a s).
Proof.
  intros a s. unfold var_set_In. induction s.
  - simpl; left; reflexivity.
  - simpl. destruct (A_eq_dec a a0).
    + rewrite e; simpl; left; reflexivity.
    + simpl; right; apply IHs.
Qed.

(** Function concerning term and var_set *)
Fixpoint get_var_set (t: term) : var_set :=
  match t with
  | (var x) => add_var_set x nil
  | (app t1 t2) => union_var_set (get_var_set t1) (get_var_set t2)
  | (abs x t') => get_var_set t'
  end.

(** Function to get all the free variables of a lambda expression
    The set of the free variables for
    - a lambda variables:         the singleton of the var itelf
    - a lambda abstractions:      the set of free variables of the body minus
                                  the singleton of the binder
    - a lambda applications:      the union of the sets of free variables of
                                  the two parts of the applications *)
Fixpoint free_var (t : term) : var_set :=
  match t with
  | (var x) => x :: nil
  | (app t1 t2) => union_var_set (free_var t1) (free_var t2)
  | (abs x t') => remove_var_set x (free_var t')
  end.

(** Some notation for set operations *)
Notation "s + x" := (add_var_set x s)
                       (at level 50, left associativity).
Notation "s - x" := (remove_var_set x s)
                      (at level 50, left associativity).
Notation "x E= s" := (in_var_set x s)
                       (at level 50, left associativity).
Notation "s1 +U+ s2" := (union_var_set s1 s2)
                          (at level 50, left associativity).
Notation "s1 +I+ s2" := (inter_var_set s1 s2)
                          (at level 50, left associativity).
Notation "s1 \ s2" := (minus_var_set s1 s2)
                        (at level 50, left associativity).

Example freevar1 : forall x: A, free_var (var x) = x :: nil.
intro x. reflexivity. Qed.

(** Predicate to determine whether a term is a redex.
    All the work is done when the argument is an application *)
Fixpoint isredex (t: term) : bool :=
  match t with
  | (var x) => false
  | (abs x b) => isredex b
  | (app t1 t2) => match t1 with
                  | (var x') => isredex t2
                  | (app t1 t2) => orb (isredex t1) (isredex t2)
                  | (abs x' b') => orb (invarset x' (freevar b')) (isredex t2)
                  end
  end.

author: n-osborne

repo: CoqLambdaCalculus


text:
(** * Collection of genaral tactics **)

(**
   In case one has a hypothesis
   [H : match e with ... => None end  =  Some ...]
   one wants to do [destruct e; discriminate H]

   [destr_discr H] does exactly this.

   However, doing this (esp. in a loop) can lead to loss of information
   in case [e] is not a variable.
   Therefore [auto_destr_discr H] does destruct and loop only if [e] is
   a variable.

   In case [e] is not a variable but one wants do do destruct anyway,
   one can use [destr_discr H] which does not apply any check.

   [destr_discr_raw check H] is an workhorse tactic used by the two
   and [accept] is an accept-all one argument tactic.
**)

Ltac destr_discr_raw check H :=
  discriminate H
  ||
  ( match type of H with
      (match ?t with _ => _ end = _) => check t; destruct t
    end;
    try discriminate H ).

Ltac auto_destr_discr H :=
  repeat destr_discr_raw is_var H.

Ltac accept H := idtac.

Ltac destr_discr H :=
  destr_discr_raw accept H.

(** For temporarily blocking some hypotheses *)

Definition HIDE (E:Prop) := E.

Ltac hide H :=
  let E := type of H in
  change (HIDE E) in H.

Definition comment {A:Type} (a:A) := True.

Notation "### X #" := (comment X) (at level 100, no associativity) : type_scope.

Ltac comment name what :=
  assert (comment what) as name by exact I.

Ltac get_last_hypothesis :=
  match goal with H: _ |- _ => constr:(H) end.

Ltac get_first_hypothesis :=
  match reverse goal with H: _ |- _ => constr:(H) end.

Ltac where_am_i :=
  repeat (match reverse goal with
          | [ H1 : comment ?X |- _ ] =>
            let H := get_last_hypothesis in
            move H1 after H; hide H1
          end);
  unfold HIDE in *.

Ltac hide_comments :=
  repeat (match goal with
          | [ H1 : comment ?X |- _ ] =>
            match reverse goal with
              [ H: _ |- _ ] =>  move H1 after H; hide H1
            end
          end);
    unfold HIDE in *.

Require Import String.
Local Open Scope string_scope.

Ltac destr_discr_info H :=
  discriminate H
  ||
  let pp := fresh "prev" in
  ( match type of H with
      (match ?t with _ => _ end = _) =>
      destruct t eqn:pp;
      let T := type of pp in
      let d := fresh "d" in
      comment d T
    end;
    try discriminate H ).

(**
    [substh id hyp] works similar to [subst id], but only in the hypothesis [hyp].
**)

Ltac substh id hyp :=
  match goal with [ H : id = _ |- _ ] => rewrite H in hyp end.

(** Cool tactic taken from
    # a stackoverflow question #
   which destructs a given hypothesis [H : ∃ (x:A) (y:B) (z:C), P x y z] into
   - [x : A]
   - [y : B]
   - [z : C]
   - [H : P x y z]
*)

Ltac do_destr H x :=
  let x := fresh x in
  let H' := fresh H in
  edestruct H as [x H'];
  try (is_var H'; clear H; rename H' into H).

Ltac destr_one_ex H :=
match type of H with
| ex (fun x => _) => do_destr H x
| forall _, ex (fun x => _) => do_destr H x
| forall _ _, ex (fun x => _) => do_destr H x
| forall _ _ _, ex (fun x => _) => do_destr H x
end.

Ltac decompose_ex H :=
  repeat destr_one_ex H.

(** [decompose_and H as (? & Y & H)].
   It destructs completely a conjunction [H] giving a name [Y]
   to the second conjunct and automatic names to the others.
   The initial conjunction is cleared.
   If [H] is not present at the end of the intropattern,
   the conjunction is not decomposed completely.
   *)
Tactic Notation "decompose_and" ident(H) :=
  decompose [and] H; clear H.

Tactic Notation "decompose_and" ident(H) "as" simple_intropattern(patt) :=
  destruct H as patt;
  try (progress decompose [and] H; clear H).

(** [ssplit] - safe split - splits _only_ conjunctions in the goal and
   only the main line. Normal [repeat split] may do some unwanted evar
   instantiations and apply constructors in other one-constructor
   inductive types *)
Ltac ssplit :=
  lazymatch goal with
  [ |- (_ /\ _) ] =>
    split; [ssplit | ssplit]
  | _ => idtac
  end.

(** [subtle] solve trivial goals _without_ instantiating evars;
   recommended for [repeat (ssplit; subtle)] *)
Ltac subtle := try match goal with [ |- ?G ] => has_evar G; fail 2 end || trivial.

Require Import JaSyntax.

(** [destruct_eq] siplifies handling of (decidable) quality tests in goals *)

Ltac destruct_eq := try match goal with
                          [ |- context [string_dec ?C ?C] ] => destruct (string_dec C C); try contradiction
                        | [ |- context [JFXId_dec ?C ?C] ] => destruct (JFXId_dec C C); try contradiction
                        | [ |- context [JFVal_dec ?C ?C] ] => destruct (JFVal_dec C C); try contradiction
                        | [ |- context [JFClassName_dec ?C ?C] ] => destruct (JFClassName_dec C C); try contradiction
                        | [ H : (?C <> ?D) |- context [string_dec ?C ?D] ] => destruct (string_dec C D); try contradiction
                        | [ H : (?C = ?D) |- context [string_dec ?C ?D] ] => destruct (string_dec C D); try contradiction
                        end.

(** [eqf] finds two equalities with identical lhs, derives new
    equality between the two rhs and simplifies it *)

Ltac eqf :=
  match goal with
    [ H1 : ?l = ?r, H2 : ?l = ?r' |- _ ] =>
      let H := fresh in
      assert (r=r') as H by congruence;
      simplify_eq H; clear H
  end.

author: jbujak

repo: jafun

save_path: github-repos/coq/jbujak-jafun


text:
Require Import HoTT.
Require Import HoTT_axioms.
Require Import Equiv_def.
Require Import V1_Param_CComega_fixpoint.
From Coq Require Import ssreflect.

Set Universe Polymorphism.

(* ########################################################### *)
(* ###        Parametricity for Inductive Types            ### *)
(* ########################################################### *)

(** Generic Lemma to prove contractibility of telescope **)

Definition IsContr_telescope {A} {P RA : A -> Type}
           {RP : forall a, RA a -> P a -> Type}
  : IsContr {a:A & RA a} ->
    (forall a H, IsContr {b : P a & RP a H b}) ->
    IsContr {a : A & {b : P a & {H : RA a & RP a H b}}}.
Proof.
  intros Ha Hb. apply (contr_equiv2 {a : A & RA a}); try apply Ha.
  apply EquivSigma. intro a. eapply Equiv_inverse.
  eapply equiv_compose. eapply swap_sigma.
  cbn. apply IsContrSigma_codomain. intro H. apply Hb.
Defined.

Ltac isFun f :=
  let x := fresh "foo" in
  intro x; induction x ;
  eapply contr_equiv2 ; try (apply Equiv_inverse; apply f);
  repeat (eapply IsContr_telescope; intros); try apply IsContr_True;
  match goal with | H : _ |- _ => eapply H end.

(*** A ⊔ B ⋈ A' ⊔ B' ***)
Inductive somme (A:Type) (B:Type) : Type :=
  |inl : A -> somme A B
  |inr : B -> somme A B.

Arguments inl {_ _} _.
Arguments inr {_ _} _.

Notation "A ⊔ B" := (somme A B) (at level 30).

Fixpoint FR_somme {A A' B B':Type} (RA : A -> A' -> Type) (RB : B -> B' -> Type)
                  (x:A ⊔ B) (y:A' ⊔ B') : Type.
Proof.
  destruct x as [a | b], y as [a' | b'].
  - exact (RA a a').
  - exact False.
  - exact False.
  - exact (RB b b').
Defined.

Definition code_somme_arg {A A' B B' : Type} (RA : A -> A' -> Type) (RB : B -> B' -> Type) (x : A ⊔ B) : Type.
  destruct x as [a | b].
  - exact ({a':A' & FR_somme RA RB (inl a) (inl a')}).
  - exact ({b':B' & FR_somme RA RB (inr b) (inr b')}).
Defined.

Definition Equiv_somme_arg {A A' B B' : Type} (RA : A -> A' -> Type) (RB : B -> B' -> Type) (x : A ⊔ B) :
  Equiv ({y : A'⊔B' & FR_somme RA RB x y}) (code_somme_arg RA RB x).
  unfold code_somme_arg. induction x as [a | b].
  * unshelve econstructor.
    - intros [y r]; destruct y as [a' | b']. exact (a'; r). inversion r.
    - unshelve eapply isequiv_adjointify.
      -- intros [a' r]. exact (inl a'; r).
      -- intros [y r]; destruct y as [a' | b'] => //=; inversion r.
      -- intros [a' r]. reflexivity.
  * unshelve econstructor.
  - intros [y r]; destruct y as [a' | b']. inversion r. exact (b'; r).
  - unshelve eapply isequiv_adjointify.
    -- intros [b' r]. exact (inr b'; r).
    -- intros [y r]; destruct y as [a' | b' ]=> //=; inversion r.
    -- intros [b' r] => //=.
Defined.

Definition IsFun_somme {A A' B B' : Type} (RA : A -> A' -> Type) (RB : B -> B' -> Type)
  (WFA : IsFun RA) (WFB : IsFun RB) : IsFun (FR_somme RA RB).
Proof.
  isFun @Equiv_somme_arg.
Defined.

Definition Somme_sym_sym {A A' B B': Type}
(RA : A -> A' -> Type) (RB : B -> B' -> Type) :
forall {x y}, FR_somme RA RB x y ≃ sym (FR_somme (sym RA) (sym RB)) x y.
Proof.
  intros x y. unshelve econstructor.
  - revert y. induction x as [a | b]; intro y; destruct y as [a' | b']; cbn;
    intro r; try (exact r).
  - unshelve eapply isequiv_adjointify.
    -- revert y. induction x as [a | b]; intro y; destruct y as [a' | b']; cbn;
    intro r; try (exact r).
    -- revert y. induction x as [a | b]; intro y; destruct y as [a' | b']; cbn;
       try reflexivity.
    -- revert y. induction x as [a | b]; intro y; destruct y as [a' | b']; cbn;
    try reflexivity.
Defined.

Definition Somme_sym_sym_bis {A A' B B': Type}
  (RA : A -> A' -> Type) (RB : B -> B' -> Type) :
  forall {x y}, FR_somme RA RB x y ≃ sym (FR_somme (sym RA) (sym RB)) x y.
Proof.
  intros x y. destruct x as [a | b], y as [a' | b']; cbn; try (apply Equiv_id).
Defined.

Definition FP_somme {A A' B B' : Type} (eA : A ⋈ A') (eB : B ⋈ B') : (A ⊔ B) ⋈ (A' ⊔ B').
Proof.
  destruct eA as [RA FA]; destruct eB as [RB FB].
  destruct FA as [WFA WFAsym]; destruct FB as [WFB WFBsym].
  unshelve econstructor.
  + exact (FR_somme RA RB).
  + unfold rel. unshelve econstructor.
    - apply IsFun_somme; assumption.
    - eapply IsFun_sym. eapply Somme_sym_sym. apply IsFun_somme.
      all: assumption.
Defined.

(*** List A ⋈ List B ***)

Inductive list (A : Type) : Type :=
    nil : list A | cons : A -> list A -> list A.

Arguments nil {_}.
Arguments cons {_} _ _.

Notation "[ ]" := nil (format "[ ]").
Notation "[ x ]" := (cons x nil).
Notation "[ x ; y ; .. ; z ]" := (cons x (cons y .. (cons z nil) ..)).

Infix "::" := cons (at level 60, right associativity).

Fixpoint FR_list {A A'} (RA : A -> A' -> Type) (l: list A) (l': list A') : Type.
Proof.
  destruct l as [ |a l], l' as [ |a' l'].
  - exact True.
  - exact False.
  - exact False.
  - exact ({H : RA a a' & FR_list A A' RA l l'}).
Defined.

Definition code_list_arg {A A' : Type} (RA : A -> A' -> Type) (x: list A) : Type.
Proof.
  destruct x as [ |a l].
  exact (FR_list RA [] []).
  exact ({a':A' &{l':list A' & FR_list RA (a::l) (a'::l')}}).
Defined.

Definition Equiv_list_arg {A A' : Type} (RA : A -> A' -> Type) (x: list A) :
  Equiv ({y : list A' & FR_list RA x y}) (code_list_arg RA x).
Proof.
  destruct x; unfold code_list_arg.
  * unshelve econstructor.
    - intros [l r]; destruct l. exact r. inversion r.
    - unshelve eapply isequiv_adjointify.
      -- intro r. exact ([]; r).
      -- intros [l r]; destruct l; cbn. reflexivity. inversion r.
      -- cbn. reflexivity.
  * unshelve econstructor.
    - intros [l r]; destruct l. inversion r. exact (a0;(l;r)).
    - unshelve eapply isequiv_adjointify.
      -- intros [a' [l' r]]. exact (a'::l'; r).
      -- intros [l r]; destruct l; cbn. inversion r. reflexivity.
      -- intros [a' [l' r]]. reflexivity.
Defined.

Definition IsFun_list (A A' : Type) (RA : A -> A' -> Type)
           (WFA : IsFun RA) : IsFun (FR_list RA).
Proof.
  isFun @Equiv_list_arg.
Defined.

Definition listR_sym_sym A A' (R : A -> A' -> Type) :
  forall l l', FR_list R l l' ≃ sym (FR_list (sym R)) l l'.
Proof.
  intros l l'. unshelve econstructor.
  - revert l'. induction l; intro l'; destruct l'; cbn; intro r; try exact r.
    exists r.1. apply IHl. exact r.2.
  - unshelve eapply isequiv_adjointify.
    -- revert l'. induction l; intro l'; destruct l'; cbn; intro r; try exact r.
       exists r.1. apply IHl. exact r.2.
    -- revert l'. induction l; intro l'; destruct l'; cbn; try reflexivity.
       intros [Xa X]. rewrite (IHl l' X). reflexivity.
    -- revert l'. induction l; intro l'; destruct l'; cbn; try reflexivity.
      + intros [Xa X]. rewrite (IHl l' X). reflexivity.
Defined.

Definition listR_sym_sym_bis A A' (R : A -> A' -> Type) :
  forall l l', FR_list R l l' ≃ sym (FR_list (sym R)) l l'.
Proof.
  intros l; induction l as [ |a l]; intro l'; induction l' as [ |a' l']; cbn; try (apply Equiv_id).
  unshelve econstructor.
  - intros [H X]. exists H. apply IHl. exact X.
  - unshelve eapply isequiv_adjointify.
    -- intros [H X]. exists H. apply IHl. exact X.
    -- intros [H X]; apply path_sigma_uncurried; unshelve econstructor; try reflexivity.
       cbn. apply e_sect.
       -- intros [H X]; apply path_sigma_uncurried; unshelve econstructor; try reflexivity.
       cbn. apply e_retr.
Defined.

Definition FP_list (A A' : Type) (eA : A ⋈ A'):
  list A ⋈ list A'.
Proof.
  unshelve econstructor. exact (FR_list (_R eA)).
  split.
  apply IsFun_list; typeclasses eauto.
  eapply IsFun_sym. eapply listR_sym_sym. apply IsFun_list.
  destruct eA as [RA FA]. destruct FA as [WF WFsym].
  exact WFsym.
Defined.

(*** tree A ⋈ tree A' ***)
Inductive tree A : Type :=
  |nil_tree : tree A
  |cons_tree : tree A -> A -> tree A -> tree A.

Arguments nil_tree {_}.
Arguments cons_tree {_} _ _ _.

Fixpoint FR_tree {A A' : Type} (RA : A -> A' -> Type) (t : tree A) (t' : tree A') : Type.
Proof.
  destruct t as [ | ls a rs], t' as [ | ls' a' rs' ].
  - exact True.
  - exact False.
  - exact False.
  - exact ({Xl : FR_tree A A' RA ls ls' & {Xa : RA a a' & FR_tree A A' RA rs rs'}}).
Defined.

Definition code_tree_arg {A A' : Type} (RA : A -> A' -> Type) (t : tree A) : Type.
Proof.
  destruct t as [ | ls a rs].
  - exact (FR_tree RA nil_tree nil_tree).
  - exact ({ls' : tree A' & {a' :A' & {rs' : tree A' & FR_tree RA (cons_tree ls a rs) (cons_tree ls' a' rs') }}}).
Defined.

Definition Equiv_tree_arg {A A' : Type} (RA : A -> A' -> Type) (t : tree A) :
      Equiv ({t' : tree A' & FR_tree RA t t'}) (code_tree_arg RA t).
Proof.
  destruct t as [ | ls a rs]; cbn.
  * unshelve econstructor.
    - intros [t' r]. destruct t' as [ | ls' a' rs'].
      exact I. destruct r.
    - unshelve eapply isequiv_adjointify.
      -- exists nil_tree. exact H.
      -- intros [t' r]. destruct t' as [ | ls' a' rs']; cbn in r; destruct r.
         reflexivity.
      -- cbn. intro x; destruct x. reflexivity.
  * unshelve econstructor.
  - intros [t' r]. destruct t' as [ | ls' a' rs'].
    destruct r. exists ls', a', rs'. exact r.
  - unshelve eapply isequiv_adjointify.
    -- intros [ls' [a' [rs' r]]]. exists (cons_tree ls' a' rs'). exact r.
    -- intros [t' r]. destruct t' as [ | ls' a' rs']; cbn in r.
        destruct r. reflexivity.
    -- intros [ls' [a' [rs' r]]]. reflexivity.
Defined.

(* Pbl IsContr_telecop limité à 2 *)
Definition IsFun_tree {A A' : Type} (RA : A -> A' -> Type) (WFA : IsFun RA): IsFun(FR_tree RA).
Proof.
  intro t. induction t;
  eapply contr_equiv2; try (eapply Equiv_inverse; apply Equiv_tree_arg).
  - apply IsContr_True.
  - cbn.
    eapply contr_equiv2. apply Equiv_inverse; eapply EquivSigma; intro ls'. apply SigmaSigma.
    cbn.
    (* utilisation telescope *)
    apply (IsContr_telescope IHt1). intros ls' Xs.
    (* décurry *)
    eapply (@contr_equiv2 ({a':A' & {rs' : tree A' & {XA : RA a a' & FR_tree RA t2 rs' }}})).
    apply (@SigmaSigma _ _ (fun a' rs' => {_ : RA a a' & FR_tree RA t2 rs'})).
    (* next *)
    apply ((IsContr_telescope) (WFA a) (fun a' XA => IHt2)).
Defined.

Definition Tree_sym_sym A A' (RA : A -> A' -> Type) :
  forall t t', FR_tree RA t t' ≃ sym (FR_tree (sym RA)) t t'.
Proof.
  intros t t'. unshelve econstructor.
  - revert t'. induction t; intro t'; destruct t'; cbn; intro r; try exact r.
    destruct r as [Xs [Xa Xr]].
      unshelve econstructor. apply IHt1; exact Xs.
      unshelve econstructor. exact Xa.
      apply IHt2; exact Xr.
  - unshelve eapply isequiv_adjointify.
    -- revert t'. induction t; intro t'; destruct t'; cbn; intro r; try exact r.
       destruct r as [Xs [Xa Xr]].
       unshelve econstructor. apply IHt1; exact Xs.
       unshelve econstructor. exact Xa.
       apply IHt2; exact Xr.
    -- revert t'. induction t; intro t'; destruct t'; cbn; intro r; try reflexivity.
       destruct r as [Xs [Xa Xr]]. rewrite (IHt1 t'1 Xs). rewrite (IHt2 t'2 Xr). reflexivity.
    -- revert t'. induction t; intro t'; destruct t'; cbn; intro r; try reflexivity.
       destruct r as [Xs [Xa Xr]]. rewrite (IHt1 t'1 Xs). rewrite (IHt2 t'2 Xr). reflexivity.
Defined.

Definition Tree_sym_sym_bis A A' (RA : A -> A' -> Type) :
  forall t t', FR_tree RA t t' ≃ sym (FR_tree (sym RA)) t t'.
Proof.
  intro t; induction t; intro t'; destruct t'; cbn; try (apply Equiv_id).
  unshelve econstructor.
  - intros [Xs [Xa Xr]].
    unshelve econstructor. apply IHt1; exact Xs.
    unshelve econstructor. exact Xa.
    apply IHt2; exact Xr.
  - unshelve eapply isequiv_adjointify.
    -- intros [Xs [Xa Xr]].
       unshelve econstructor. apply IHt1; exact Xs.
       unshelve econstructor. exact Xa.
       apply IHt2; exact Xr.
    -- intros [Xs [Xa Xr]]. cbn. rewrite e_sect. rewrite e_sect. reflexivity.
    -- intros [Xs [Xa Xr]]. cbn. rewrite e_retr. rewrite e_retr. reflexivity.
Defined.

Definition FP_tree {A A':Type} (eA : A ⋈ A') : tree A ⋈ tree A'.
Proof.
  unshelve econstructor.
  exact (FR_tree (_R eA)).
  unshelve econstructor.
  * unfold rel. apply IsFun_tree. typeclasses eauto.
  * eapply IsFun_sym. apply Tree_sym_sym. apply IsFun_tree.
    destruct eA as [RA [WFA WFAsym]]. exact WFAsym.
Defined.

(*** ∑(a:A) B ⋈ ∑(a':A') B' ***)

(* rappel
Inductive sigT {A:Type} (P:A -> Type) : Type :=
    existT : forall x:A, P x -> sigT P.

Notation "{ x : A & P }" := (sigT (A:=A) (fun x => P)) : type_scope.
Notation "x .1" := (projT1 x) (at level 3).
Notation "x .2" := (projT2 x) (at level 3).
Notation " ( x ; p ) " := (existT _ x p).

Definition EqSigma {A : Type} {P : A -> Type} (w w' : {a:A & P a}) : Equiv (w = w') {p: w .1 = w' .1 & p # (w .2) = w' .2}.
Proof. *)

Fixpoint FR_sigma {A A'} {B : A -> Type} {B' : A' -> Type}
      (RA : A -> A' -> Type)
      (RB : forall (a:A) (a':A') (H:RA a a'), B a -> B' a' -> Type)
      (x : {a: A & B a}) (y:{a':A' & B' a'}) : Type.
Proof.
  destruct x as [a b], y as [a' b'].
  exact ({H: RA a a' & RB a a' H b b'}).
Defined.

Definition code_sigma_arg {A A':Type} {B : A -> Type} {B' : A' -> Type}
      (RA : A -> A' -> Type)
      (RB : forall (a:A) (a':A') (H:RA a a'), B a -> B' a' -> Type)
      (x: {a:A & B a}) : Type.
Proof.
  destruct x as [a b].
  exact ({a' : A' & {b' : B' a' & FR_sigma RA RB (a;b) (a';b')}}).
Defined.

Definition Equiv_sigma_arg {A A':Type} {B : A -> Type} {B' : A' -> Type}
  (RA : A -> A' -> Type) (RB : forall (a:A) (a':A') (H:RA a a'), B a -> B' a' -> Type)
  (x: {a:A & B a}) :
  Equiv ({y:{a':A' & B' a'} & FR_sigma RA RB x y}) (code_sigma_arg RA RB x).
Proof.
  destruct x as [a b]. unshelve econstructor.
  - intros [y r]. destruct y as [a' b']; cbn.
    exists a'. exists b'. exact r.
  - unshelve eapply isequiv_adjointify.
    -- intros [a' [b' r]]. exact ((a';b'); r).
    -- intros [y r]; destruct y; cbn. try reflexivity.
    -- intros [a' [b' r]]; cbn. try reflexivity.
Defined.

Definition IsFun_sigma {A A'} {B : A -> Type} {B' : A' -> Type}
      {RA : A -> A' -> Type}
      {RB : forall a a' (H:RA a a'), Rel (B a) (B' a')}
      (WFA : IsFun RA)
      (WFB : forall a a' (H: RA a a'), IsFun(RB a a' H)) :
      IsFun (FR_sigma RA RB).
Proof.
  isFun @Equiv_sigma_arg.
Defined.

Definition Sigma_sym_sym {A A'} {P : A -> Type} {P' : A' -> Type}
  {RA : A -> A' -> Type}
  {RB : forall a a' (H:RA a a'), Rel (P a) (P' a')} :
  forall z w, (FR_sigma RA RB z w) ≃ sym (FR_sigma (sym RA) (fun x y e => sym (RB y x e))) z w.
Proof.
  intros z w. unshelve econstructor.
  - revert w; induction z as [a b]; intro w; destruct w as [a' b']; cbn.
    intros [H X]. exists H. exact X.
  - unshelve eapply isequiv_adjointify.
    -- revert w; induction z as [a b]; intro w; destruct w as [a' b']; cbn.
    intros [H X]. exists H. exact X.
    -- revert w; induction z as [a b]; intro w; destruct w as [a' b']; cbn.
       intros [H X]. reflexivity.
    -- revert w; induction z as [a b]; intro w; destruct w as [a' b']; cbn.
       intros [H X]. reflexivity.
Defined.

Definition Sigma_sym_sym_bis {A A'} {P : A -> Type} {P' : A' -> Type}
  {RA : A -> A' -> Type}
  {RB : forall a a' (H:RA a a'), Rel (P a) (P' a')} :
  forall z w, (FR_sigma RA RB z w) ≃ sym (FR_sigma (sym RA) (fun x y e => sym (RB y x e))) z w.
Proof.
  intros z w. destruct z as [a b], w as [a' b']. cbn.
  unshelve econstructor.
  - intros [H X]. exists H. exact X.
  - unshelve eapply isequiv_adjointify.
    -- intros [H X]. exists H. exact X.
    -- intros [H X]; reflexivity.
    -- intros [H X]; reflexivity.
Defined.

Definition FP_sigma (A A' : Type) (B : A -> Type) (B' : A' -> Type)
    (eA : A ⋈ A')
    (eB : forall (a:A) (a':A') (H: (_R eA) a a'), B a ⋈ B' a') :
  {a:A & B a} ⋈ {a':A' & B' a'}.
Proof.
  destruct eA as [RA FA]. destruct FA as [WFA WFAsym].
  unshelve econstructor. unfold Rel.
  * eapply (FR_sigma RA).
    intros a a' H b b'. exact (_R (eB a a' H) b b').
  * split.
    + apply IsFun_sigma. exact WFA.
      intros a a' H. destruct (eB a a' H) as [RB FB]. destruct FB as [WFB WFBsym].
      exact WFB.
    + eapply IsFun_sym. eapply Sigma_sym_sym. apply IsFun_sigma.
      - exact WFAsym.
      - intros a' a H. destruct (eB a a' H) as [RB FB].
      destruct FB as [WFB WFBsym]. exact WFBsym.
Defined.

author: CoqHott

repo: parametricity-a-la-carte


text:
(*** Weak AVL Trees ***)

(*+
See "Rank-Balanced Trees" by Haeupler, Sen, Tarjan
[http://www.cs.princeton.edu/~sssix/papers/rb-trees-talg.pdf].
*)

(* A non-automated (actually, semi-automated) version of wavl.v, with no
tailored specific solver tactics.  Note that the general "boom" and "ss"
automation tactics are still used throughout. *)
Set Ltac Profiling.
Reset Ltac Profile.
Require Import mindless.elist.
Require Import mindless.ezbool.
Require Import mindless.utils.
Require Import mindless.hypiter.

Generalizable All Variables.

Set Default Goal Selector "all".

Context {A : Set}.

Context {ordA : Ordered A}.

Context {compare : A -> A -> comparison}.

Context {compare_spec : forall x y, CompareSpecT (eq x y) (lt x y) (lt y x) (compare x y)}.

Notation "x =<> y" := (compare_spec x y) (at level 70, only parsing).

Notation EL := ##(list A).
Notation EZ := ##Z.
Notation EB := ##bool.

Open Scope E_scope.

Inductive wavltree (k : EZ)(pg lg rg : EB)(c : EL) : Set :=
| Node(g : bool)(d : A)
      (_: #g = pg)
      `(_: c = lc++[d]++rc)
      `(lw : wavltree (k - #1 - ^lg) lg llg lrg lc)
      `(rw : wavltree (k - #1 - ^rg) rg rlg rrg rc)
      (leaf_rule: k = #1 -> lg = #false \/ rg = #false)
      (_: Esorted c)
| Missing(_: c = [])(_: k = - #1)(_: lg = #false)(_: rg = #false).

(**********************************************************************)

(*Tactic notations to make the proofs more readable:*)

Tactic Notation "??" constr(H) :=
  (tryif (is_var H; try (clear H;
                         fail 1))
    then case_eq H
    else case H);
  dintros.

Tactic Notation "??" constr(H) "on" constr(H') :=
  case H with (1:=H'); dintros.

Tactic Notation "just" tactic1(tac) := let x := tac in exact x.

Ltac left_child w :=
  lazymatch type of w with
    wavltree _ _ _ _ (?C++[_]++_) =>
    lazymatch goal with
      L:wavltree _ _ _ _ C |- _ => L
    end
  end.

Notation "'left_child' w" := ltac:(just left_child w)
                                    (at level 199, no associativity, only parsing).

Ltac right_child w :=
  lazymatch type of w with
    wavltree _ _ _ _ (_++[_]++?C) =>
    lazymatch goal with
      R:wavltree _ _ _ _ C |- _ => R
    end
  end.

Notation "'right_child' w" := ltac:(just right_child w)
                                     (at level 199, no associativity, only parsing).

Ltac datum w :=
  lazymatch type of w with
    wavltree _ _ _ _ (_++[?D]++_) => D
  end.

Notation "'datum' w" := ltac:(just datum w)
                               (at level 199, no associativity, only parsing).

Ltac gap w :=
  lazymatch type of w with
    wavltree _ # ?G _ _ _ => G
  end.

Notation "'gap' w" := ltac:(just gap w)
                             (at level 199, no associativity, only parsing).

Notation "'pick' x" := ltac:(just pick x)
                             (at level 199, no associativity, only parsing).

(**********************************************************************)

Section Lemmas.

  Lemma wavl_min_rank`(w : wavltree k g lg rg c) : k >= - #1.
  Proof.
    induction w. boom.
  Qed.

  Lemma wavl_node_min_rank`(w : wavltree k g lg rg c) : c <> [] -> k >= #0.
  Proof.
    ?? w. 1:pose proof (wavl_min_rank (left_child w)). boom.
  Qed.

  Lemma wavl_node_nonempty`(w : wavltree k g lg rg c) : k >= #0 -> c <> [].
  Proof.
    ?? w. boom.
  Qed.

  Lemma missing_contents`(w : wavltree (- #1) g lg rg c) : c = [].
  Proof.
    pose proof (wavl_node_min_rank w) as H.
    ?? w. boom.
  Qed.

  Lemma missing_rank`(w : wavltree k g lg rg []) : k = - #1.
  Proof.
    ?? w.
    - fnenil.
    - reflexivity.
  Qed.

  Lemma wavl_is_sorted`(w : wavltree k g lg rg c) : Esorted c.
  Proof.
    ?? w.
    - assumption.
    - repeat econstructor.
  Qed.

End Lemmas.

Ltac bang_setup_tactic ::= idtac;
  let f H :=
      (lazymatch type of H with
       | wavltree _ _ _ _ _ =>
         first [apply missing_rank in H
               |apply wavl_node_min_rank in H; [|assumption||fnenil]
               |apply wavl_min_rank in H]
       | _ => idtac
       end) in
  allhyps_introing f.

Ltac ss_setup_tactic := idtac;
  let f H := (try apply wavl_is_sorted in H) in
  allhyps_introing f.

Ltac ss := ss_setup_tactic; unerase; solve[solve_sorted].

(**********************************************************************)

Section Check_Leaf_Rule.

  Local Set Asymmetric Patterns.

  Local Definition is_leaf`(w : wavltree k g lg rg c) : bool :=
    match w with
    | Node _ _ _ _ _ _ _ _ (Missing _ _ _ _) _ _ (Missing _ _ _ _) _ _ => true
    | _ => false
    end.

  Local Ltac destruct_match := idtac;
    match goal with |- context[match ?X with _ => _ end] => destruct X end.

  Local Lemma leaf_rule_works`(w : wavltree k g lg rg c) : k = #0 <-> is_leaf w = true.
  Proof.
    unfold is_leaf.
    repeat destruct_match.
    boom.
  Qed.

End Check_Leaf_Rule.

(**********************************************************************)

Section Find.

  Inductive findResult(x : A)(c : EL) : Set :=
  | Found`(_: c = lc++[x]++rc)
  | NotFound(_: ENotIn x c).

  Fixpoint find(x : A)`(w : wavltree k g lg rg c) : findResult x c.
  Proof.
    ?? w.
    - ?? (x =<> (datum w)).
      + eapply Found. reflexivity.
      + ?? (find x) on (left_child w).
        * eapply Found. rootify x. reflexivity.
        * eapply NotFound. ss.
      + ?? (find x) on (right_child w).
        * eapply Found. rootify x. reflexivity.
        * eapply NotFound. ss.
    - eapply NotFound. ss.
  Qed.

End Find.

Section SetGap.

  Definition setgap`(w : wavltree k ig lg rg c)(og : bool) : wavltree k #og lg rg c.
  Proof.
    ?? w.
    - eapply Node. reflexivity + eassumption.
    - eapply Missing. reflexivity.
  Qed.

End SetGap.

Section GetGap.

  Definition getgap`(w : wavltree k g lg rg c) : { g' | c <> [] -> #g' = g}.
  Proof.
    ?? w.
    - eexists. reflexivity.
    - exists false. boom.
  Qed.

  Definition getgap2`(w : wavltree k g lg rg c) : { g' | k >= #0 -> #g' = g}.
  Proof.
    ?? w.
    - eexists. reflexivity.
    - exists false. boom.
  Qed.

End GetGap.

Section IsGap.

  Notation "x ?= y" := (Bool.bool_dec x y) (only parsing).

  Definition isgap`(w : wavltree k g lg rg c)(g' : bool) : {k >= #0 /\ #g' = g} + {k= - #1 \/ #g' <> g}.
  Proof.
    ?? w.
    - ?? (g' ?= (gap w)).
      + left. boom.
      + right. boom.
    - right. boom.
  Qed.

End IsGap.

Section IsMissing.

  Definition isMissing`(w : wavltree k g lg rg c) : {c = [] /\ k = - #1} + {c <> [] /\ k >= #0}.
  Proof.
    ?? w.
    - right. boom.
    - left. boom.
    Qed.

End IsMissing.

Ltac start_node := eapply Node; [reflexivity|reflexivity|..].
Ltac missing := eapply Missing; [reflexivity|boom|reflexivity|reflexivity].
Ltac use w := idtac; force refine w by boom.
Ltac use_regap w := idtac; force refine (setgap w _) by boom.
Ltac use_node := idtac;
  lazymatch goal with
    w: wavltree _ _ _ _ ?C |- wavltree _ _ _ _ ?C => use w + use_regap w
  end.
Ltac finish := idtac;
  match goal with
  | |- Esorted _ => ss
  | _ => boom
  end.

Section Insert_Rotations.

  Definition irot1`(lw : wavltree k #false llg lrg lc)(x : A)`(rw : wavltree (k - #2) #true rlg rrg rc)
    : llg = Enegb lrg -> Esorted(lc++[x]++rc) -> forall g, wavltree k #g #false #false (lc++[x]++rc).
  Proof.
    (* lw is higher than rw (k > k-2), so it makes sense to examine lw first *)
    ?? lw.
    - (* The right child of lw, rw0, needs to be combined somehow with rw.  rw0
         might be at the same height or 1 above rw, so that needs to be
         determined first.  But, if we first examine rw0 before examining its
         gap, we can eliminate the case when it is missing *)
      ?? (right_child lw).
      + (* rw0 is not missing, so examine its gap now *)
        ?? (gap (right_child lw)).
        * (* rw0 has a gap, so it is at k-2, the same as rw, which means the two
             can be combined easily with the result not havng a gap, so still
             fitting under k, rooted where lw already is *)
          rootify (datum lw). start_node.
          -- exact (left_child lw).
          -- rootify x. start_node.
             ++ use_regap (right_child lw).
             ++ use_regap rw.
             ++ finish.
             ++ finish.
          -- finish.
          -- finish.
        * (* rw0 has no gap, so we have to split it up with its left child lw1
             pairing with lw0, the regapped left child of lw, and its right
             child rw1 pairing with regapped rw, with the new root where rw0
             is *)
          rootify (datum (right_child lw)). start_node.
          -- start_node.
             ++ use_regap (left_child lw).
             ++ use (left_child (right_child lw)).
             ++ finish.
             ++ finish.
          -- start_node.
             ++ use (right_child (right_child lw)).
             ++ use_regap rw.
             ++ finish.
             ++ finish.
          -- finish.
          -- finish.
      + (* rw0 is missing - note that its sequence is now [] *)
        assert (k = #1) as -> by boom. rsimp.
        (* note that his implies rw is missing as well, because its height is -1 *)
        apply missing_contents in rw as ->.
        rootify (datum lw). start_node.
        * use (left_child lw).
        * start_node.
          -- missing.
          -- missing.
          -- finish.
          -- finish.
        * finish.
        * finish.
    - (* lw is missing, but that's not possible because rw is lower, so there is
         a contradiction *)
      boom.
  Qed.

  Definition irot2`(lw : wavltree (k - #2) #true llg lrg lc)(x : A)`(rw : wavltree k #false rlg rrg rc)
    : Enegb rlg = rrg -> Esorted(lc++[x]++rc) -> forall g, wavltree k #g #false #false (lc++[x]++rc).
  Proof.
    ?? rw.
    - ?? (left_child rw).
      + ?? (gap (left_child rw)).
        * rootify (datum rw). start_node.
          -- start_node.
             ++ use_node. (*use_regap lw.*)
             ++ use_node. (*use_regap (left_child rw).*)
             ++ finish.
             ++ finish.
          -- use_node. (*use (right_child rw).*)
          -- finish.
          -- finish.
        * rootify (datum (left_child rw)). start_node.
          -- start_node.
             ++ use_node. (*use_regap lw.*)
             ++ use_node. (*use (left_child (left_child rw)).*)
             ++ finish.
             ++ finish.
          -- start_node.
             ++ use_node. (*use (right_child (left_child rw)).*)
             ++ use_node. (*use_regap (right_child rw).*)
             ++ finish.
             ++ finish.
          -- finish.
          -- finish.
      + assert (k = #1) as -> by boom. rsimp. apply missing_contents in lw as ->.
        rootify (datum rw). start_node.
        * start_node.
          -- missing.
          -- missing.
          -- finish.
          -- finish.
        * use_node. (*use (right_child rw).*)
        * finish.
        * finish.
    - boom.
  Qed.

End Insert_Rotations.

Ltac unerase_gaps :=
  subst;
  let f H :=
      try
        lazymatch type of H with
          wavltree _ ?G _ _ _ =>
          is_var G;
          case (getgap H);
          let X := fresh in
          let G' := fresh in
          intros G' X;
          first [specialize (X ltac:(assumption||fnenil))
                |specialize (X (wavl_node_nonempty H ltac:(boom)))];
          rewrite <-X in *;
          clear X G;
          rename G' into G
        end in
    allhyps_td f. (*cannot be allhyps_introing because of rewrite?*)

Section Insert.

  Inductive insertedHow(ik ok : EZ)(ig og olg org : EB) : Set :=
  | ISameK(_: ok = ik)(_: og = ig)
  | IWasMissing(_: ik = - #1)(_: ok = #0)(_: og = #false)
  | IHigherK(_: ik >= #0)(_: ok = ik + #1)(_: olg = Enegb org)(_: og = #false).

  Inductive insertResult(x: A)(k : EZ)(g lg rg : EB)(c : EL) : Set :=
  | Inserted`(_: c = lc++rc)
            `(ow: wavltree ok og olg org (lc++[x]++rc))
            `(_: insertedHow k ok g og olg org)
  | FoundByInsert`(_: c = lc++[x]++rc).

  Lemma nilnilnil : [] = [] ++ [] :> EL.
  Proof.
    rewrite Eapp_nil_l.
    reflexivity.
  Qed.

  Ltac tree_with x := idtac;
    match goal with
      H:wavltree _ _ _ _ ?C |- _ =>
      lazymatch C with context[x] => H end
    end.

  Notation "'tree_with' x" := ltac:(just tree_with x)
                                    (at level 199, no associativity, only parsing).

  Fixpoint insert(x : A)`(w : wavltree k g lg rg c) : insertResult x k g lg rg c.
  Proof.
    ?? w.
    - ?? (x =<> (datum w)).
      + eapply FoundByInsert. reflexivity.
      + ?? (insert x) on (left_child w).
        * ?? (pick insertedHow).
          -- assoc 0. eapply Inserted.
             ++ reflexivity.
             ++ rootify (datum w). start_node.
               ** use_node. (*use (tree_with x).*)
                ** use_node. (*use (right_child w).*)
                ** finish.
                ** finish.
             ++ eapply ISameK. boom.
          -- ?? (isMissing (right_child w)).
             ++ assoc 0. eapply Inserted.
                ** reflexivity.
                ** rootify (datum w). start_node.
                   --- use_node. (*use (tree_with x).*)
                   --- missing.
                   --- finish.
                   --- finish.
                ** eapply IHigherK. boom.
             ++ assoc 0. eapply Inserted.
                ** reflexivity.
                ** rootify (datum w). start_node.
                   --- use_node. (*use (tree_with x).*)
                   --- use_node. (*use (right_child w).*)
                   --- finish.
                   --- finish.
                ** eapply ISameK. boom.
          -- unerase_gaps. ?? (gap (left_child w)).
             ++ assoc 0. eapply Inserted.
                ** reflexivity.
                ** rootify (datum w). start_node.
                   --- use_node. (*use (tree_with x).*)
                   --- use_node. (*use (right_child w).*)
                   --- finish.
                   --- finish.
                ** eapply ISameK. boom.
             ++ ?? (isgap (right_child w) false).
                ** assoc 0. eapply Inserted.
                   --- reflexivity.
                   --- rootify (datum w). start_node.
                       +++ use_node. (*use (tree_with x).*)
                       +++ use_node. (*use_regap (right_child w).*)
                       +++ finish.
                       +++ finish.
                   --- eapply IHigherK. boom.
                ** assoc 0. eapply Inserted.
                   --- reflexivity.
                   --- rootify (datum w). eapply irot1.
                       +++ use_node. (*use (tree_with x).*)
                       +++ use_node. (*use (right_child w).*)
                       +++ finish.
                       +++ finish.
                   --- eapply ISameK. boom.
        * rootify x. eapply FoundByInsert. reflexivity.
      + ?? (insert x) on (right_child w).
        * ?? (pick insertedHow).
          -- assoc 2. eapply Inserted.
             ++ reflexivity.
             ++ rootify (datum w). start_node.
                ** use_node. (*use (left_child w).*)
                ** use_node. (*use (tree_with x).*)
                ** finish.
                ** finish.
             ++ eapply ISameK. boom.
          -- ?? (isMissing (left_child w)).
             ++ assoc 2. eapply Inserted.
                ** reflexivity.
                ** rootify (datum w). start_node.
                   --- missing.
                   --- use_node. (*use (tree_with x).*)
                   --- finish.
                   --- finish.
                ** eapply IHigherK. boom.
             ++ assoc 2. eapply Inserted.
                ** reflexivity.
                ** rootify (datum w). start_node.
                   --- use_node. (*use (left_child w).*)
                   --- use_node. (*use (tree_with x).*)
                   --- finish.
                   --- finish.
                ** eapply ISameK. boom.
          -- unerase_gaps. ?? (gap (right_child w)).
             ++ assoc 2. eapply Inserted.
                ** reflexivity.
                ** rootify (datum w). start_node.
                   --- use_node. (*use (left_child w).*)
                   --- use_node. (*use (tree_with x).*)
                   --- finish.
                   --- finish.
                ** eapply ISameK. boom.
             ++ ?? (isgap (left_child w) false).
                ** assoc 2. eapply Inserted.
                   --- reflexivity.
                   --- rootify (datum w). start_node. all: [>use_node|use_node|..].
                    (* +++ use_regap (left_child w).
                       +++ use (tree_with x). *)
                       +++ finish.
                       +++ finish.
                   --- eapply IHigherK. boom.
                ** assoc 2. eapply Inserted.
                   --- reflexivity.
                   --- rootify (datum w). eapply irot2.
                       +++ use_node. (*use (left_child w).*)
                       +++ use_node. (*use (tree_with x).*)
                       +++ finish.
                       +++ finish.
                   --- eapply ISameK.  boom.
        * rootify x. eapply FoundByInsert. reflexivity.
    - eapply Inserted.
      + eapply nilnilnil.
      + start_node.
        * missing.
        * missing.
        * finish.
        * finish.
      + eapply IWasMissing. boom.
  Qed.

End Insert.

(**********************************************************************)

Section TryLowering.

  Inductive tryLoweringResult(k : EZ)(g lg rg : EB)(c : EL) : Set :=
  | TLlowered(_: lg = #true)(_: rg = #true)(ow: wavltree (k - #1) g #false #false c)
  | TLtooLow(_: lg = #false \/ rg = #false).

  Definition tryLowering`(w : wavltree k g lg rg c) : tryLoweringResult k g lg rg c.
  Proof.
    ?? w.
    - ?? (isgap (left_child w) true).
      + ?? (isgap (right_child w) true).
        * eapply TLlowered.
          -- reflexivity.
          -- reflexivity.
          -- start_node.
             ++ use_node. (*use_regap (left_child w).*)
             ++ use_node. (*use_regap (right_child w).*)
             ++ finish.
             ++ finish.
        * eapply TLtooLow. boom.
      + eapply TLtooLow. boom.
    - eapply TLtooLow. boom.
  Qed.

End TryLowering.

Inductive deletedHow(ik ok : EZ)(ig og : EB) : Set :=
| DSameK(_: ok = ik)(_: og = ig)
| DLowerK(_:  ok = ik - #1)(_: og = #true).

Inductive delpair(k : EZ)(g : EB)(c : EL) : Set :=
| Delout`(dh : deletedHow k ok g og)`(ow : wavltree ok og olg org c).

Section Delete_Rotations.

  Definition drot1`(lw : wavltree (k - #3) #true llg lrg lc)(x : A)`(rw : wavltree (k - #1) #false rlg rrg rc)
    : rlg = #false \/ rrg = #false -> Esorted(lc++[x]++rc) -> forall g, delpair k #g (lc++[x]++rc).
  Proof.
    ?? rw.
    - ?? (left_child rw).
      + ?? (isgap (right_child rw) false).
        * eapply Delout.
          -- apply DSameK.
             ++ reflexivity.
             ++ reflexivity.
          -- rootify (datum rw). start_node.
             ++ start_node.
                ** use_node. (*use lw.*)
                ** use_node. (*use (left_child rw).*)
                ** finish.
                ** finish.
             ++ use_node. (*use_regap (right_child rw).*)
             ++ finish.
             ++ finish.
        * eapply Delout.
          -- apply DSameK.
             ++ reflexivity.
             ++ reflexivity.
          -- rootify (datum (left_child rw)). start_node.
             ++ start_node. 1-2:use_node.
             (* ** use_node. (*use_regap lw.*)
                ** use_node. (*use (left_child (left_child rw)).*)*)
                ** finish.
                ** finish.
             ++ start_node.
                ** use_node. (*use (right_child (left_child rw)).*)
                ** use_node. (*use_regap (right_child rw).*)
                ** finish.
                ** finish.
             ++ finish.
             ++ finish.
      + assert (k = #2) as -> by boom. rsimp. apply missing_contents in lw as ->.
        eapply Delout.
        * apply DSameK.
          -- reflexivity.
          -- reflexivity.
        * rootify (datum rw). start_node.
          -- start_node.
             ++ missing.
             ++ missing.
             ++ finish.
             ++ finish.
          -- use_node. (*use_regap (right_child rw).*)
          -- finish.
          -- finish.
    - boom.
  Qed.

  Definition drot2`(lw : wavltree (k - #1) #false llg lrg lc)(x : A)`(rw : wavltree (k - #3) #true rlg rrg rc)
    : llg = #false \/ lrg = #false -> Esorted(lc++[x]++rc) -> forall g, delpair k #g (lc++[x]++rc).
  Proof.
    ?? lw.
    - ?? (right_child lw).
      + ?? (isgap (left_child lw) false).
        * eapply Delout.
          -- apply DSameK.
             ++ reflexivity.
             ++ reflexivity.
          -- rootify (datum lw). start_node.
             ++ use_node. (*use_regap (left_child lw).*)
             ++ rootify x. start_node.
                ** use_node. (*use (right_child lw).*)
                ** use_node. (*use rw.*)
                ** finish.
                ** finish.
             ++ finish.
             ++ finish.
        * eapply Delout.
          -- apply DSameK.
             ++ reflexivity.
             ++ reflexivity.
          -- rootify (datum (right_child lw)). start_node.
             ++ start_node. 1-2:use_node.
             (* ** use_node. (*use_regap (left_child lw).*)
                ** use_node. (*use (left_child (right_child lw)).*)*)
                ** finish.
                ** finish.
             ++ start_node.
                ** use_node. (*use (right_child (right_child lw)).*)
                ** use_node. (*use_regap rw.*)
                ** finish.
                ** finish.
             ++ finish.
             ++ finish.
      + assert (k = #2) as -> by boom. rsimp. apply missing_contents in rw as ->.
        eapply Delout.
        * apply DSameK.
          -- reflexivity.
          -- reflexivity.
        * rootify (datum lw). start_node.
          -- use_node. (*use_regap (left_child lw).*)
          -- start_node.
             ++ missing.
             ++ missing.
             ++ finish.
             ++ finish.
          -- finish.
          -- finish.
    - boom.
  Qed.

End Delete_Rotations.

Section Delete_Minimum.

  Inductive delminResult(k : EZ)(g : EB)(c : EL) : Set :=
    MinDeleted(min : A)`(_: c = [min]++rc)(dp : delpair k g rc).

  Fixpoint delmin`(w : wavltree k g lg rg c) : k >= #0 -> delminResult k g c.
  Proof.
    ?? w.
    - ?? (isMissing (left_child w)).
      + eapply MinDeleted.
        * rewrite Eapp_nil_l. reflexivity.
        * eapply Delout.
          -- apply DLowerK.
             ++ reflexivity.
             ++ reflexivity.
          -- use_node. (*use_regap rw.*)
      + ?? delmin on (left_child w).
        * boom.
        * ?? (pick delpair). ?? (pick deletedHow).
          -- eapply MinDeleted.
             ++ assoc 0. reflexivity.
             ++ eapply Delout.
                ** apply DSameK.
                   --- reflexivity.
                   --- reflexivity.
                ** start_node.
                   --- use_node. (*use ow.*)
                   --- use_node. (*use rw.*)
                   --- finish.
                   --- finish.
          -- ?? (isgap (right_child w) false).
             ++ ?? (isgap (left_child w) true).
                ** ?? (tryLowering (right_child w)).
                   --- eapply MinDeleted.
                       +++ assoc 0. reflexivity.
                       +++ eapply Delout.
                           *** apply DLowerK.
                               ---- reflexivity.
                               ---- reflexivity.
                           *** start_node.
                               ---- use_node. (*use ow.*)
                               ---- use_node. (*use ow0.*)
                               ---- finish.
                               ---- finish.
                   --- eapply MinDeleted.
                       +++ assoc 0. reflexivity.
                       +++ eapply drot1.
                           *** use_node. (*use ow.*)
                           *** use_node. (*use rw.*)
                           *** finish.
                           *** finish.
                ** eapply MinDeleted.
                   --- assoc 0. reflexivity.
                   --- eapply Delout.
                       +++ apply DSameK.
                           *** reflexivity.
                           *** reflexivity.
                       +++ start_node.
                           *** use_node. (*use ow.*)
                           *** use_node. (*use rw.*)
                           *** finish.
                           *** finish.
             ++ unerase_gaps. eapply MinDeleted.
                ** assoc 0. reflexivity.
                ** eapply Delout.
                   --- apply DLowerK.
                       +++ reflexivity.
                       +++ reflexivity.
                   --- start_node.
                       +++ use_node. (*use_regap ow.*)
                       +++ use_node. (*use_regap rw.*)
                       +++ finish.
                       +++ finish.
    - boom.
  Qed.

End Delete_Minimum.

Section Delete_Maximum.

  Inductive delmaxResult(k : EZ)(g : EB)(c : EL) : Set :=
   MaxDeleted(max : A)`(_: c = lc++[max])(dp : delpair k g lc).

  Fixpoint delmax`(w : wavltree k g lg rg c) : k >= #0 -> delmaxResult k g c.
  Proof.
    ?? w.
    - ?? (isMissing (right_child w)).
      + eapply MaxDeleted.
        * rewrite Eapp_nil_r. reflexivity.
        * eapply Delout.
          -- apply DLowerK.
             ++ reflexivity.
             ++ reflexivity.
          -- use_node. (*use_regap lw.*)
      + ?? delmax on (right_child w).
        * boom.
        * ?? (pick delpair). ?? (pick deletedHow).
          -- eapply MaxDeleted.
             ++ assoc 2. reflexivity.
             ++ eapply Delout.
                ** apply DSameK.
                   --- reflexivity.
                   --- reflexivity.
                ** start_node.
                   --- use_node. (*use lw.*)
                   --- use_node. (*use ow.*)
                   --- finish.
                   --- finish.
        -- ?? (isgap (left_child w) false).
           ++  ?? (isgap (right_child w) true).
               ** ?? (tryLowering (left_child w)).
                  --- eapply MaxDeleted.
                      +++ assoc 2. reflexivity.
                      +++ eapply Delout.
                          *** apply DLowerK.
                              ---- reflexivity.
                              ---- reflexivity.
                          *** start_node.
                              ---- use_node. (*use ow0.*)
                              ---- use_node. (*use ow.*)
                              ---- finish.
                              ---- finish.
                  --- eapply MaxDeleted.
                      +++ assoc 2. reflexivity.
                      +++ eapply drot2.
                          *** use_node. (*use lw.*)
                          *** use_node. (*use ow.*)
                          *** finish.
                          *** finish.
               ** eapply MaxDeleted.
                  --- assoc 2. reflexivity.
                  --- eapply Delout.
                      +++ apply DSameK.
                          *** reflexivity.
                          *** reflexivity.
                      +++ start_node.
                          *** use_node. (*use lw.*)
                          *** use_node. (*use ow.*)
                          *** finish.
                          *** finish.
           ++ unerase_gaps. eapply MaxDeleted.
              ** assoc 2. reflexivity.
              ** eapply Delout.
                 --- apply DLowerK.
                     +++ reflexivity.
                     +++ reflexivity.
                 --- start_node.
                     +++ use_node. (*use_regap lw.*)
                     +++ use_node. (*use_regap ow.*)
                     +++ finish.
                     +++ finish.
    - boom.
  Qed.

End Delete_Maximum.

Section Delete.

  Inductive deleteResult(x : A)(k : EZ)(g : EB)(c : EL) : Set :=
  | Deleted`(_: c = lc++[x]++rc)(dp : delpair k g (lc++rc))
  | DNotFound(_: ENotIn x c).

  Fixpoint delete(x : A)`(w : wavltree k g lg rg c) : deleteResult x k g c.
  Proof.
    ?? w.
    - ?? (x =<> (datum w)).
      + ?? (isMissing (left_child w)).
        * eapply Deleted.
          -- reflexivity.
          -- eapply Delout.
             ++ apply DLowerK.
                ** reflexivity.
                ** reflexivity.
             ++ rewrite Eapp_nil_l. use_node. (*use_regap rw.*)
        * ?? (isMissing (right_child w)).
          -- eapply Deleted.
             ++ reflexivity.
             ++ eapply Delout.
                ** apply DLowerK.
                   --- reflexivity.
                   --- reflexivity.
                ** rewrite Eapp_nil_r. use_node. (*use_regap lw.*)
          -- unerase_gaps. ?? (gap (left_child w)).
             ++ ?? (delmin (right_child w)).
                ** boom.
                ** ?? (pick delpair). ?? (pick deletedHow).
                   --- eapply Deleted.
                       +++ reflexivity.
                       +++ eapply Delout.
                           *** apply DSameK.
                               ---- reflexivity.
                               ---- reflexivity.
                           *** start_node.
                               ---- use_node. (*use lw.*)
                               ---- use_node. (*use ow.*)
                               ---- finish.
                               ---- finish.
                   --- eapply Deleted.
                       +++ reflexivity.
                       +++ eapply Delout.
                           *** apply DLowerK.
                               ---- reflexivity.
                               ---- reflexivity.
                           *** start_node.
                               ---- use_node. (*use_regap lw.*)
                               ---- use_node. (*use_regap ow.*)
                               ---- finish.
                               ---- finish.
             ++ ?? (delmax (left_child w)).
                ** boom.
                ** ?? (pick delpair). ?? (pick deletedHow).
                   --- eapply Deleted.
                       +++ reflexivity.
                       +++ eapply Delout.
                           *** apply DSameK.
                               ---- reflexivity.
                               ---- reflexivity.
                           *** assoc 0. start_node.
                               ---- use_node. (*use ow.*)
                               ---- use_node. (*use rw.*)
                               ---- finish.
                               ---- finish.
                   --- eapply Deleted.
                       +++ reflexivity.
                       +++ eapply Delout.
                           *** apply DSameK.
                               ---- reflexivity.
                               ---- reflexivity.
                           *** assoc 0. start_node.
                               ---- use_node. (*use ow.*)
                               ---- use_node. (*use rw.*)
                               ---- finish.
                               ---- finish.
      + ?? (delete x) on (left_child w).
        * ?? (pick delpair). ?? (pick deletedHow).
          -- eapply Deleted.
             ++ rootify x. reflexivity.
             ++ eapply Delout.
                ** apply DSameK.
                   --- reflexivity.
                   --- reflexivity.
                ** rootify d. start_node.
                   --- use_node. (*use ow.*)
                   --- use_node. (*use rw.*)
                   --- finish.
                   --- finish.
          -- unerase_gaps. ?? (gap (left_child w)).
             ++ unerase_gaps. ?? (gap (right_child w)).
                ** eapply Deleted.
                   --- rootify x. reflexivity.
                   --- eapply Delout.
                       +++ apply DLowerK.
                           *** reflexivity.
                           *** reflexivity.
                       +++ rootify d. start_node.
                           *** use_node. (*use ow.*)
                           *** use_node. (*use_regap rw.*)
                           *** finish.
                           *** finish.
                ** ?? (tryLowering (right_child w)).
                   --- eapply Deleted.
                       +++ rootify x. reflexivity.
                       +++ eapply Delout.
                           *** apply DLowerK.
                               ---- reflexivity.
                               ---- reflexivity.
                           *** rootify d. start_node.
                               ---- use_node. (*use ow.*)
                               ---- use_node. (*use ow0.*)
                               ---- finish.
                               ---- finish.
                   --- eapply Deleted.
                       +++ rootify x. reflexivity.
                       +++ rootify d. eapply drot1.
                           *** use_node. (*use ow.*)
                           *** use_node. (*use rw.*)
                           *** finish.
                           *** finish.
             ++ ?? (isMissing (right_child w)).
                ** eapply Deleted.
                   --- rootify x. reflexivity.
                   --- rootify d. eapply Delout.
                       +++ apply DLowerK.
                           *** reflexivity.
                           *** reflexivity.
                       +++ start_node.
                           *** use_node. (*use_regap ow.*)
                           *** missing.
                           *** finish.
                           *** finish.
                ** eapply Deleted.
                   --- rootify x. reflexivity.
                   --- eapply Delout.
                       +++ apply DSameK.
                           *** reflexivity.
                           *** reflexivity.
                       +++ rootify d. start_node.
                           *** use_node. (*use ow.*)
                           *** use_node. (*use rw.*)
                           *** finish.
                           *** finish.
        * eapply DNotFound. ss.
      + ?? (delete x) on (right_child w).
        * ?? (pick delpair). ?? (pick deletedHow).
          -- eapply Deleted.
             ++ rootify x. reflexivity.
             ++ rootify d. eapply Delout.
                ** apply DSameK.
                   --- reflexivity.
                   --- reflexivity.
                ** start_node.
                   --- use_node. (*use lw.*)
                   --- use_node. (*use ow.*)
                   --- finish.
                   --- finish.
          -- unerase_gaps. ?? (gap (right_child w)).
             ++ unerase_gaps. ?? (gap (left_child w)).
                ** eapply Deleted.
                   --- rootify x. reflexivity.
                   --- rootify d. eapply Delout.
                       +++ apply DLowerK.
                           *** reflexivity.
                           *** reflexivity.
                       +++ start_node.
                           *** use_node. (*use_regap lw.*)
                           *** use_node. (*use ow.*)
                           *** finish.
                           *** finish.
                ** ?? (tryLowering (left_child w)).
                   --- eapply Deleted.
                       +++ rootify x. reflexivity.
                       +++ rootify d. eapply Delout.
                           *** apply DLowerK.
                               ---- reflexivity.
                               ---- reflexivity.
                           *** start_node.
                               ---- use_node. (*use ow0.*)
                               ---- use_node. (*use ow.*)
                               ---- finish.
                               ---- finish.
                   --- eapply Deleted.
                       +++ rootify x. reflexivity.
                       +++ rootify d. eapply drot2.
                           *** use_node. (*use lw.*)
                           *** use_node. (*use ow.*)
                           *** finish.
                           *** finish.
             ++ ?? (isMissing (left_child w)).
                ** eapply Deleted.
                   --- rootify x. reflexivity.
                   --- rootify d. eapply Delout.
                       +++ apply DLowerK.
                           *** reflexivity.
                           *** reflexivity.
                       +++ start_node.
                           *** missing.
                           *** use_node. (*use_regap ow.*)
                           *** finish.
                           *** finish.
                ** eapply Deleted.
                   --- rootify x. reflexivity.
                   --- rootify d. eapply Delout.
                       +++ apply DSameK.
                           *** reflexivity.
                           *** reflexivity.
                       +++ start_node.
                           *** use_node. (*use lw.*)
                           *** use_node. (*use ow.*)
                           *** finish.
                           *** finish.
        * eapply DNotFound. ss.
    - eapply DNotFound. ss.
  Qed.

End Delete.

Set Printing Width 120.
Show Ltac Profile CutOff 1.

Require Import ExtrOcamlBasic.

Extract Inductive delpair => "( * )" [ "" ].
Extract Inductive delminResult => "( * )" [ "" ].
Extract Inductive delmaxResult => "( * )" [ "" ].

Extraction Inline negb.

Extract Inlined Constant Bool.bool_dec => "(=)".

Extraction "wavl_noauto.ml" find insert delete.

(* Local Variables: *)
(* company-coq-local-symbols: (("++" . ?⧺) ("Esorted" . ?⊿) ("#" . ?◻) ("wavltree" . ?🎄) ("[]" . ?∅) ("^" . ?⋄) ("^#" . ?⟎) ("Enegb" . ?¬) ("true" . ?Ṫ) ("false" . ?Ḟ) ("EL" . ?Ḷ) ("EB" . ?Ḅ) ("EZ" . ?Ẓ)) *)
(* End: *)

author: jonleivent


text:
(** * Higher-order recursion, an example with finite branching trees *)

From Equations Require Import Equations.
Require Import Examples.Fin.

Inductive ho : Set :=
| base : nat -> ho
| lim : forall n : nat, (fin n -> ho) -> ho.
Derive NoConfusion for ho.

Equations lift_fin {n : nat} (f : fin n) : fin (S n) :=
lift_fin fz := fz;
lift_fin (fs f) := fs (lift_fin f).

Equations maxf (n : nat) (f : fin n -> nat) : nat :=
maxf 0 f := 0;
maxf (S n) f := max (f (gof n)) (maxf n (fun y : fin n => f (lift_fin y))).

Equations horec_struct (x : ho) : nat :=
horec_struct (base n) := n;
horec_struct (lim k f) := maxf k (fun x => horec_struct (f x)).

Derive Subterm for ho.

Equations horec (x : ho) : nat by wf x ho_subterm :=
horec (base n) := n;
horec (lim k f) := maxf k (fun x => horec (f x)).

Definition horec_test : horec (lim 7 (fun fs => base (fog fs))) = 6 := eq_refl.

repo: Coq-Equations