Early preview of the Algorithmic with OCaml book

Community
, ,
1

Please report bugs, bad English & nonsenses.
But do not report omissions (it is work-in-progress plus it’s not an ocaml bible).

Why the book is not bottom up, instead some concepts are used without explained ?

  • Because some notions (what is the unit type ? what is a queue ?) are considered easy-enough to go without saying.

What will be in the missing chapter 6 ?

  • Type polymorphism, universal quantification, Stdlib.compare, weak polymorphism, constrained polymorphism, phantom types, type variance.

What will be in the chapters 12 and more ?

  • High performance lexing
  • Recursive-descent parsing
  • The art of searching
  • Detailed construction of the ERic 0.3 application

Will the source files go to a repository ?

  • No. The source files are already included in the zip archive.
10 Likes
2

Is it desirable that each and every contribution is attached to it’s contributor ?

Does anyone knowns :

  • the real life name of dividee ?
  • the real life name of the contributor to La Lettre de Caml n°5 (caml-light code pages 10 & 11) ?

The chapter 8.6. Braun min-heap is redundant with the one at chapter 4.16.
Should i replace it by a Skew heap instead ?

3

Hey @SpiceGuid, I was hoping to post sooner once I had proven all the theorems you listed, but have been caught up with research so haven’t had the chance to work on this recently.

Seeing as you’re close to finishing the book, lest my work be for naught, I thought I might as well share what I have had the chance to do so far (see below):

I’ve proven the key properties for interval, union, filter and intersection. A couple of the theorems were too weak in their assumptions (in particular they made no assumptions about the ordering of the tree), so I had to strengthen them.

If I have some free time in the following weeks, I think I’ll try finishing the remaining properties (for disjoint, difference and remove).

(* un arbre est soit vide soit une séparation en deux *)
Inductive tree : Set :=
  | Empty: tree
  | Fork: tree -> nat -> tree -> tree.

Require Import Arith.Arith_base.

(* nombre de strahler *)
Fixpoint strahler t :=
  match t with
  | Empty => 0
  | Fork l n r =>
      let sl := strahler l in
      let sr := strahler r in
      if beq_nat sl sr then S sl else max sl sr    
  end.
   
(* recherche d'un entier n dans un arbre t *)
Fixpoint member_of n t :=
  match t with
  | Empty => false     (* absent *)
  | Fork l m r =>
      match n ?= m with
      | Eq => true     (* on l'a trouvé *)
      | Lt => member_of n l (* on cherche à gauche *)
      | Gt => member_of n r (* on cherche à droite *)
      end
  end.

(* insertion d'un entier n dans un arbre t *)
Fixpoint add n t :=
  match t with
  | Empty => Fork Empty n Empty  (* on crée un singleton *)
  | Fork l m r =>
      match n ?= m with
      | Eq => t                  (* déjà présent *)
      | Lt => Fork (add n l) m r (* on insère à gauche *)
      | Gt => Fork l m (add n r) (* on insère à droite *)
      end
  end.

(* extraction de l'intervalle [low,high] de l'arbre t *)
Fixpoint interval low high t :=
  match t with
  | Empty => Empty
  | Fork l n r =>
      match high ?= n with
      | Lt => interval low high l
      | Gt | Eq =>
          match low ?= n with
          | Gt => interval low high r
          | Lt | Eq => Fork (interval low high l) n (interval low high r)
          end
      end
  end.
  
(* c'est là qu'est défini le type list *)
Require Import Lists.List.

(* conversion de l'arbre t en une liste triée *)
Fixpoint to_list acc t :=
  match t with
  | Empty => acc
  | Fork l n r => to_list (n::to_list acc r) l
  end.

(* trouve le plus petit élément de l'arbre t *)
Fixpoint minimum acc t :=
  match t with
  | Empty => acc
  | Fork l n r => minimum n l  
  end.

(* supprime le plus petit élément de l'arbre t *)
Fixpoint remove_minimum la na ra :=
  match la with
  | Empty => ra
  | Fork lb nb rb => Fork (remove_minimum lb nb rb) na ra
  end.

(* agglomère les arbres ta et tb *)
(* les éléments de ta doivent être strictement inférieurs aux éléments de tb *)
Fixpoint concat ta tb :=
  match ta,tb with
  | _,Empty => ta
  | Empty,_ => tb
  | _,Fork lb nb rb =>
      Fork ta (minimum nb lb) (remove_minimum lb nb rb)
  end.

(* supprime l'élément n de l'arbre t *)
Fixpoint remove n t :=
  match t with
  | Empty => Empty
  | Fork l m r =>
      match n ?= m with
      | Lt => Fork (remove n l) m r
      | Gt => Fork l m (remove n r)
      | Eq => concat l r
      end
  end.

(* filtre l'arbre t suivant le prédicat cond *)
Fixpoint filter (cond : nat -> bool) t := 
  match t with
  | Empty => Empty
  | Fork l n r =>
      if cond n then Fork (filter cond l) n (filter cond r)
      else concat (filter cond l) (filter cond r)	
  end.

(* nombres d'éléments de l'arbre t *)
Fixpoint cardinal t :=
  match t with
  | Empty => 0
  | Fork l _ r => cardinal l + 1 + cardinal r
  end.
	
(* c'est là qu'est défini l'opérateur && *)
Require Import Bool.Bool.

Require Import Coq.Program.Wf.

Require Import Lia.
(* l'arbre ta est-il un sous-ensemble de l'arbre tb ? *)
Program Fixpoint subset (ta : tree) (tb : tree) {measure (cardinal ta + cardinal tb)} : bool :=
  match ta,tb with
  | Empty,_ => true
  | _,Empty => false
  | Fork la na ra,Fork lb nb rb => 
      match na ?= nb with
      | Lt => subset (Fork la na Empty) lb && subset ra tb
      | Gt => subset (Fork Empty na ra) rb && subset la tb
      | Eq => subset la lb && subset ra rb
       end
  end.
Next Obligation. Proof. simpl; lia. Qed.
Next Obligation. Proof. simpl; lia. Qed.
Next Obligation. Proof. simpl; lia. Qed.
Next Obligation. Proof. simpl; lia. Qed.
Next Obligation. Proof. simpl; lia. Qed.
Next Obligation. Proof. simpl; lia. Qed.



(* inclusion réciproque *)
Definition equal ta tb :=
  subset ta tb && subset tb ta.  
  
(* découpe t en deux parties inférieures et supérieures à n *)
Fixpoint split n t :=
  match t with
  | Empty => (Empty,false,Empty)
  | Fork l m r =>
      match n ?= m with
      | Lt => let '(la,present,ra) := split n l in (la,present,Fork ra m r)
      | Gt => let '(lb,present,rb) := split n r in (Fork l m lb,present,rb)
      | Eq => (l,true,r)
      end
  end.

(* fusionne les arbres ta et tb *)
Fixpoint union ta tb :=
  match ta,tb with
  | _,Empty => ta
  | Empty,_ => tb
  | Fork la na ra,_ => 
      let '(lb,_,rb) := split na tb
      in Fork (union la lb) na (union ra rb)
  end.

Fixpoint intersection ta tb :=
  match ta,tb with
  | _,Empty | Empty,_ => Empty
  | Fork la na ra,_ => 
      let '(lb,present,rb) := split na tb in
      if present then Fork (intersection la lb) na (intersection ra rb)
      else concat (intersection la lb) (intersection ra rb)
  end.

Fixpoint disjoint ta tb :=
  match ta,tb with
  | _,Empty | Empty,_ => true
  | Fork la na ra,_ => 
      let '(lb,present,rb) := split na tb in
      if present then false
      else disjoint la lb && disjoint ra rb
  end.

Fixpoint difference ta tb :=
  match ta,tb with
  | _,Empty => ta
  | Empty,_ => Empty
  | Fork la na ra,_ => 
      let '(lb,present,rb) := split na tb in
      if present then concat (difference la lb) (difference ra rb)
      else Fork (difference la lb) na (difference ra rb)
  end.

Inductive member : nat -> tree -> Prop :=
  | root_member :
      forall l n r,
      member n (Fork l n r)
  | left_member :
      forall m n l r,
      member n l ->
      member n (Fork l m r)
  | right_member :
      forall m n l r,
      member n r ->
      member n (Fork l m r).

Lemma member_compose:
  forall l m r n,
    member n l \/ member n r \/ (n =? m = true) ->
     member n (Fork l m r).
Proof.
  intros l m r n H.
  destruct H as [H | [H | ]].
  - apply left_member; auto.
  - apply right_member; auto.
  - destruct (Nat.eqb_spec n m) as [H | H].
    rewrite <- H; apply root_member.
    inversion H0.
Qed.

Lemma member_decompose:
  forall l m r n,
    member n (Fork l m r) ->
    member n l \/ member n r \/ (n =? m = true).
Proof.
  intros l m r n H.
  remember (Fork l m r) as node eqn:H_eq.
  destruct H as [ l' n r' | |]; inversion H_eq as [[H1 H2 H3]].
  - right; right; rewrite <- H2; apply Nat.eqb_refl. 
  - left; rewrite H1 in *;  auto. 
  - right;left; rewrite H3 in *; auto.
Qed.

Lemma member_property_split:
  forall l m r n,
    member n (Fork l m r) <->
    member n l \/ member n r \/ (n =? m = true).
Proof.
  intros l m r n; split.
  - apply member_decompose.
  - apply member_compose.
Qed.

Theorem add_main_property :
  forall n t, member n (add n t).
Proof.
  intros n t. induction t.
  (* Empty *)
  unfold add.
    apply root_member.
  (* Fork *)
  unfold add. remember (n ?= n0) as cmp.
  destruct cmp.
    (* Eq *)
    symmetry in Heqcmp.
    apply (nat_compare_eq n n0) in Heqcmp.
    subst n0. apply root_member.
    (* Lt *)
    apply left_member. exact IHt1.
    (* Gt *)
    apply right_member. exact IHt2.
Qed.

Theorem add_is_conservative :
  forall m n t, member m t -> member m (add n t).
Proof.
  intros m n t H. induction t. 
  (* Empty *)
  unfold add.
    apply left_member. exact H.
  (* Fork *)
  remember (Fork t1 n0 t2) as node.
  destruct H.
  (* root_member *)
  unfold add. destruct (n ?= n1).
    apply root_member.
    apply root_member.
    apply root_member.
  (* left_member *)
  inversion Heqnode. rewrite H1 in H.
  unfold add. destruct (n ?= n0).
    apply left_member. exact H.
    apply IHt1 in H. apply left_member. exact H.
    apply left_member. exact H.
  (* right_member *)
  inversion Heqnode. rewrite H3 in H.
  unfold add. destruct (n ?= n0).
    apply right_member. exact H.
    apply right_member. exact H.
    apply IHt2 in H. apply right_member. exact H.
Qed.

Inductive tree_less : tree -> nat -> Prop :=
  | empty_tree_less :
      forall b, tree_less Empty b
  | fork_tree_less :
      forall l m r b,
      tree_less l b -> tree_less r b -> m < b ->
      tree_less (Fork l m r) b.
 
Inductive tree_more : tree -> nat -> Prop :=
  | empty_tree_more :
      forall a, tree_more Empty a
  | fork_tree_more :
      forall l m r a,
      tree_more l a -> tree_more r a -> m > a ->
      tree_more (Fork l m r) a.
 
Inductive tree_ordered : tree -> Prop :=
  | empty_tree_ordered :
      tree_ordered Empty
  | fork_tree_ordered :
      forall l m r,
      tree_ordered l -> tree_ordered r ->
      tree_less l m -> tree_more r m ->
      tree_ordered (Fork l m r).

Lemma tree_ordered_compose:
  forall l m r,
    tree_ordered l /\ tree_ordered r /\ tree_less l m /\ tree_more r m ->
     tree_ordered (Fork l m r).
Proof.
  intros l m r [H1 [H2 [H3 H4]]].
  apply fork_tree_ordered; auto.
Qed.

Lemma tree_ordered_decompose:
  forall l m r,
    tree_ordered (Fork l m r) ->
    tree_ordered l /\ tree_ordered r /\ tree_less l m /\ tree_more r m.
Proof.
  intros l m r H; inversion H; subst.
  split; auto.
Qed.

Lemma tree_ordered_property_split:
  forall l m r,
    tree_ordered (Fork l m r) <->
    tree_ordered l /\ tree_ordered r /\ tree_less l m /\ tree_more r m.
Proof.
  intros l m r; split.
  - apply tree_ordered_decompose.
  - apply tree_ordered_compose.
Qed.


Fact tree_less_upper_bound:
  forall t n, tree_less t n <-> forall m, member m t -> m < n.
Proof.
  split.
  (* -> *)
  intros Hless m Hm. induction t.
  inversion Hm.
  inversion Hm; inversion Hless; subst; auto.
  (* <- *)
  intros H. induction t.
    constructor.
    constructor.
      apply IHt1. intros m Hm. apply H. apply left_member. assumption.
      apply IHt2. intros m Hm. apply H. apply right_member. assumption.
      apply H. apply root_member.
Qed.

Fact tree_more_lower_bound:
  forall t n, tree_more t n <-> forall m, member m t -> m > n.
Proof.
  split.
  (* -> *)
  intros Hmore m Hm. induction t.
  inversion Hm.
  inversion Hm; inversion Hmore; subst; auto.
  (* <- *)
  intros H. induction t.
    constructor.
    constructor.
      apply IHt1. intros m Hm. apply H. apply left_member. assumption.
      apply IHt2. intros m Hm. apply H. apply right_member. assumption.
      apply H. apply root_member.
Qed.

(* Require Import Arith.Lt Arith.Gt. *)

Lemma member_left:
  forall l m r n, tree_ordered (Fork l m r) -> member n (Fork l m r) -> n < m -> member n l.
Proof.
  intros l m r n Hord Hmem Hlt.
  inversion Hord; subst; clear Hord.
  inversion Hmem; subst; clear Hmem.
    contradict Hlt. apply lt_irrefl.
    assumption.
    apply tree_more_lower_bound with (m:=n) in H5.
      contradict H5. apply gt_asym. assumption.
      assumption.
Qed.
 
Lemma member_right:
  forall l m r n, tree_ordered (Fork l m r) -> member n (Fork l m r) -> n > m -> member n r.
Proof.
  intros l m r n Hord Hmem Hlt.
  inversion Hord; subst; clear Hord.
  inversion Hmem; subst; clear Hmem.
    contradict Hlt. apply lt_irrefl.
    apply tree_less_upper_bound with (m:=n) in H4.
      contradict H4. apply lt_asym. assumption. assumption.
    assumption.
Qed.

Lemma add_preserves_less:
  forall t n m, tree_less t n -> m < n -> tree_less (add m t) n.
Proof.
  induction t; intros; inversion H; subst; clear H.
  repeat constructor. assumption.
  simpl. destruct (m ?= n); constructor; auto.
Qed.
 
Lemma add_preserves_more:
  forall t n m, tree_more t n -> m > n -> tree_more (add m t) n.
Proof.
  induction t; intros; inversion H; subst; clear H.
  repeat constructor. assumption.
  simpl. destruct (m ?= n); constructor; auto.
Qed.

Theorem add_preserves_order :
  forall t, tree_ordered t ->
  forall n, tree_ordered (add n t).
Proof.
  induction t; intros.
  (* Empty *)
  simpl. repeat constructor.
  (* Fork *)
  simpl. remember (n0 ?= n) as cmp. symmetry in Heqcmp.
  destruct cmp.
    assumption.
    inversion H; subst; clear H. constructor; auto.
      apply nat_compare_lt in Heqcmp. apply add_preserves_less; assumption.
    inversion H; subst; clear H. constructor; auto.
      apply nat_compare_gt in Heqcmp. apply add_preserves_more; assumption.
Qed.

Theorem interval_membership_sound_property :
  forall low high n t, member n (interval low high t) -> member n t /\ low <= n <= high.
Proof.
  intros low high n t.
  induction t; simpl.
  * intro H; inversion H.
  * case_eq (Nat.compare high n0); intros H_high.
    case_eq (Nat.compare low n0); intros H_low.
  + rewrite member_property_split; intros H.
    case H as [H|[H|H]].
    ++ pose proof (IHt1 H) as H_t1; case H_t1 as [H_mem H_rng].
       split; auto; apply left_member; assumption.
    ++ pose proof (IHt2 H) as H_t2; case H_t2 as [H_mem H_rng].
       split; auto; apply right_member; assumption.
    ++ rewrite (Nat.compare_eq _ _ H_high).
       rewrite (Nat.compare_eq _ _ H_low).
       rewrite (beq_nat_true _ _ H); split; auto.
       apply root_member.
  + rewrite member_property_split; intros H.
    case H as [H|[H|H]].
    ++ pose proof (IHt1 H) as H_t1; case H_t1 as [H_mem H_rng].
       split; auto; apply left_member; assumption.
    ++ pose proof (IHt2 H) as H_t2; case H_t2 as [H_mem H_rng].
       split; auto; apply right_member; assumption.
    ++ rewrite (Nat.compare_eq _ _ H_high).
       pose proof (nat_compare_Lt_lt _ _ H_low) as H_lt.
       rewrite (beq_nat_true _ _ H); split; auto.
       apply root_member.
       split; auto.
       apply Nat.lt_le_incl; assumption.
  + intro H; pose proof (IHt2 H) as [H1 H2]; split; auto.
    apply right_member; assumption.
  + intro H; pose proof (IHt1 H) as [H1 H2]; split; auto.
    apply left_member; assumption.
  + case_eq (Nat.compare low n0); intros H_low.
    ++ rewrite member_property_split; intros H.
       case H as [H|[H|H]].
       pose proof (IHt1 H) as [H1 H2]; split; auto.
       apply left_member; assumption.
       pose proof (IHt2 H) as [H1 H2]; split; auto.
       apply right_member; assumption.
       rewrite (Nat.compare_eq _ _ H_low).
       rewrite (beq_nat_true _ _ H); split; auto.
       apply root_member.
       split; auto.
       apply Nat.lt_le_incl; apply Nat.compare_gt_iff; assumption.
    ++ rewrite member_property_split; intros H.
       case H as [H|[H|H]].
       pose proof (IHt1 H) as [H1 H2]; split; auto.
       apply left_member; assumption.
       pose proof (IHt2 H) as [H1 H2]; split; auto.
       apply right_member; assumption.
       rewrite (beq_nat_true _ _ H); split; auto.
       apply root_member.
       split; auto.
       apply Nat.lt_le_incl; apply Nat.compare_lt_iff; assumption.
       apply Nat.lt_le_incl; apply Nat.compare_gt_iff; assumption.
    ++ intro H; pose proof (IHt2 H) as [H1 H2]; split; auto.
       apply right_member; assumption.
Qed.


Theorem interval_membership_complete_property :
  forall low high n t, member n t /\ low <= n <= high /\ tree_ordered t -> member n (interval low high t).
Proof.
  intros low high n t.
  generalize low high n; clear low high n; induction t as [| l IHl n0 r IHr].
  - intros low high n H; case H as []; simpl; auto.
  - intros low high n; simpl.
    case_eq (Nat.compare high n0); intros H_high.
    case_eq (Nat.compare low n0); intros H_low.
    ++ rewrite member_property_split; intros H.
       case H as [[H0 | [H0 | H0]] [H1 H2]].
       inversion H2; subst; apply left_member; apply IHl; split; auto.
       inversion H2; subst; apply right_member; apply IHr; split; auto.
       rewrite (beq_nat_true _ _ H0); apply root_member.
    ++ rewrite member_property_split; intros H.
       case H as [[H0 | [H0 | H0]] [H1 H2]].
       inversion H2; subst; apply left_member; apply IHl; split; auto.
       inversion H2; subst; apply right_member; apply IHr; split; auto.
       rewrite (beq_nat_true _ _ H0); apply root_member.
    ++ rewrite (Nat.compare_eq _ _ H_high); intros H.
       case H as [H0 [H1 H2]]; inversion H2; subst.
       pose proof (nat_compare_Gt_gt _ _ H_low).
       lia.
    ++ pose proof (nat_compare_Lt_lt _ _ H_high) as H_high'; intros H.
       case H as [H0 [H1 H2]]; inversion H2; subst.
       apply IHl; split; auto.
       apply (member_left l n0 r n); auto.
       lia.
    ++ case_eq (Nat.compare low n0); intros H_low.
       ** rewrite member_property_split; intros H.
          case H as [[H0 | [H0 | H0]] [H1 H2]].
          inversion H2; subst; apply left_member; apply IHl; split; auto.
          inversion H2; subst; apply right_member; apply IHr; split; auto.
          rewrite (beq_nat_true _ _ H0); apply root_member.
       ** rewrite member_property_split; intros H.
          case H as [[H0 | [H0 | H0]] [H1 H2]].
          inversion H2; subst; apply left_member; apply IHl; split; auto.
          inversion H2; subst; apply right_member; apply IHr; split; auto.
          rewrite (beq_nat_true _ _ H0); apply root_member.
       ** pose proof (nat_compare_Gt_gt _ _ H_high) as H_high' .
          pose proof (nat_compare_Gt_gt _ _ H_low) as H_low' .
          intros H.
          case H as [H0 [H1 H2]]; inversion H2; subst.
          apply IHr; split; auto.
          apply (member_right l n0 r n); auto.          
          lia.
Qed.


(* specification des opérations ensemblistes *)
Theorem interval_main_property :
  forall low high n t, tree_ordered t ->  member n (interval low high t) <-> member n t /\ low <= n <= high.
Proof.
  intros low high n t Hord; split.
  apply interval_membership_sound_property.
  intro H; case H as [H1 H2]; apply interval_membership_complete_property; split; auto.
Qed.

Theorem remove_minimum_preserves_membership :
  forall n m l r, tree_ordered (Fork l n r) -> member m (Fork l n r) ->
                  minimum m (Fork l n r) <> m -> member m (remove_minimum l n r).
Proof.
  intros n m l r.
  generalize n m r; clear n m r.
  induction l as [|ll IHll ln lr IHlr]; intros n m r; simpl.
  - rewrite tree_ordered_property_split; intros [Hord1 [Hord2 [Hord3 Hord4]]].
    rewrite member_property_split; intros Hmem.
    case Hmem as [Hmem| [Hmem|Hmem]]; auto.
    * inversion Hmem.
    * apply beq_nat_true in Hmem; rewrite Hmem; intros Hneq; contradict Hneq; auto.
  - rewrite tree_ordered_property_split; intros [Hord1 [Hord2 [Hord3 Hord4]]].
    rewrite member_property_split; intros Hmem.
    case Hmem as [Hmem| [Hmem|Hmem]]; auto.
    * intros Hmin; apply left_member; apply IHll; auto.
    * intros Hmin; apply right_member; auto.
    * apply beq_nat_true in Hmem; rewrite Hmem; intros Hmin; apply root_member.
Qed.

Theorem remove_minimum_preserves_membership_strong :
  forall n m l r, member m (Fork l n r) ->
                  minimum m (Fork l n r) <> m -> member m (remove_minimum l n r).
Proof.
  intros n m l r.
  generalize n m r; clear n m r.
  induction l as [|ll IHll ln lr IHlr]; intros n m r; simpl.
  - rewrite member_property_split; intros Hmem.
    case Hmem as [Hmem| [Hmem|Hmem]]; auto.
    * inversion Hmem.
    * apply beq_nat_true in Hmem; rewrite Hmem; intros Hneq; contradict Hneq; auto.
  - rewrite member_property_split; intros Hmem.
    case Hmem as [Hmem| [Hmem|Hmem]]; auto.
    * intros Hmin; apply left_member; apply IHll; auto.
    * intros Hmin; apply right_member; auto.
    * apply beq_nat_true in Hmem; rewrite Hmem; intros Hmin; apply root_member.
Qed.

Theorem concat_preserves_membership_left :
  forall m l r, member m l -> member m (concat l r).
Proof.
  intros m l r; case l; simpl.
  - intros H; inversion H.
  - intros H; case r; auto.
    intros; apply left_member; auto.
Qed.

Theorem concat_preserves_membership_internal_strong : forall m l n r ta,
  member m (Fork l n r) ->
  member m (Fork ta (minimum n l) (remove_minimum l n r)).
Proof.
  intros m l n r ta.
  intros Hmem.
  pose proof (remove_minimum_preserves_membership_strong n m l r Hmem) as Hmin; simpl in Hmin.
  case_eq ((minimum n l) =? m).
  - intros Hminl; apply beq_nat_true in Hminl; rewrite Hminl; apply root_member.
  - intros Hminl; apply beq_nat_false in Hminl; apply right_member; apply Hmin; auto.
Qed.

Theorem concat_preserves_membership_right_strong :
  forall m l r, member m r -> member m (concat l r).
Proof.
  intros m l r; generalize m l; clear m l; induction r as [| rl IHrl rn rr IHrr]; simpl; intros m l.
  - intros H; inversion H.
  - rewrite member_property_split; intros [Hmem | [ Hmem | Hmem]]; simpl.
    * case l; simpl; try apply left_member; auto.
      intros ll ln lr. apply concat_preserves_membership_internal_strong; auto; apply left_member; auto.
    * case l; simpl; try apply right_member; auto.
      intros ll ln lr; apply concat_preserves_membership_internal_strong; auto; apply right_member; auto.
    * apply beq_nat_true in Hmem; rewrite Hmem; clear Hmem.
      case l; simpl; try apply root_member; auto.      
      intros ll ln lr; apply concat_preserves_membership_internal_strong; auto; apply root_member; auto.      
Qed.

Theorem member_property_remove_minimum_split :
  forall m l n r, member m (remove_minimum l n r) -> member m l \/ member m r \/ (m =? n) = true.
Proof.
  intros m l n r; generalize m r n; clear m r n; induction l as [| ll IHll ln lr IHlr]; simpl; intros m r n; auto.
  rewrite member_property_split; intros [Hmem|[Hmem|Hmem]]; auto; left;
  pose proof (IHll m lr ln Hmem) as [H1 | [H1 | H1]]; auto.
  apply left_member; auto.
  apply right_member; auto.
  apply beq_nat_true in H1; rewrite H1 in *; apply root_member.
Qed.

Theorem member_property_concat_split :
  forall m l r, member m (concat l r) -> member m l \/ member m r.
Proof.
  intros m l r; generalize m r; clear m r; induction l as [| ll IHll ln lr IHlr]; simpl; intros m r.
  * case r; auto.
  * case r as [| rl rn rr]; auto.
    rewrite member_property_split; intros [Hmem|[Hmem|Hmem]].
    ** left; auto.
    ** apply member_property_remove_minimum_split in Hmem.
       case Hmem as [Hmem|[Hmem|Hmem]].
       *** right; apply left_member; auto.
       *** right; apply right_member; auto.
       *** apply beq_nat_true in Hmem; rewrite Hmem in *; right; apply root_member.
    ** apply beq_nat_true in Hmem; rewrite Hmem in *; right.
       clear.
       generalize rl rn rr; clear rl rn rr; intros l.
       induction l as [|ll IHll ln lr IHlr]; simpl; try apply root_member.
       intros n r; apply left_member; apply IHll.
Qed.

Theorem remove_is_conservative :
  forall m n t, member m t /\ m <> n -> member m (remove n t).
Proof.
  intros m n t; generalize m n; clear m n; induction t as [| l IHl n0 r IHr]; simpl; auto; intros m n.
  - intros H; inversion H; auto.
  - rewrite member_property_split; intros [[H | [H | H]] Hneq].
    * case_eq (Nat.compare n n0); intros H_n0.
      ** apply concat_preserves_membership_left; auto.
      ** apply left_member; apply IHl; auto.
      ** apply left_member; auto.
    * case_eq (Nat.compare n n0); intros H_n0.
      ** apply concat_preserves_membership_right_strong; auto.
      ** apply right_member; auto.
      ** apply right_member; apply IHr; auto.
    * apply beq_nat_true in H; rewrite H in *; clear H.
      case_eq (Nat.compare n n0); intros H_n0.
      ** apply nat_compare_eq in H_n0; rewrite H_n0 in Hneq; contradict Hneq; auto.
      ** apply root_member; auto.
      ** apply root_member; auto.
Qed.      

Theorem filter_main_property :
  forall n t cond, member n (filter cond t) <-> member n t /\ cond n = true.
Proof.
  intros n t cond; split.
  - generalize n cond; clear n cond; induction t as [| l IHl n r IHr]; intros m cond; simpl.
    * intros H; inversion H.
    * case_eq (cond n); intros Hcond; simpl.
      ** rewrite member_property_split; intros [Hmem|[Hmem|Hmem]].
         *** pose proof (IHl m cond Hmem) as [H1 H2].
             split; auto; apply left_member; auto.
         *** pose proof (IHr m cond Hmem) as [H1 H2].
             split; auto; apply right_member; auto.
         *** apply beq_nat_true in Hmem; rewrite Hmem in *; split; auto; apply root_member.
      ** simpl; intros H; apply member_property_concat_split in H.
         case H as [H|H].
         *** pose proof (IHl m cond H) as [H1 H2].
             split; auto; apply left_member; auto.
         *** pose proof (IHr m cond H) as [H1 H2].
             split; auto; apply right_member; auto.
  - intros [Hl Hr]; generalize Hr Hl; clear Hl Hr.
    generalize n cond; clear n cond; induction t as [| l IHl n r IHr]; intros m cond; simpl; auto.
    * intros Hcondm; case_eq (cond n); intros Hcond; simpl.
      ** rewrite member_property_split; intros [Hmem|[Hmem|Hmem]].
         *** apply left_member; apply IHl; auto.
         *** apply right_member; apply IHr; auto.
         *** apply beq_nat_true in Hmem; rewrite Hmem in *; apply root_member.
      ** rewrite member_property_split; intros [Hmem|[Hmem|Hmem]].
         *** apply concat_preserves_membership_left; apply IHl; auto.
         *** apply concat_preserves_membership_right_strong; apply IHr; auto.
         *** apply beq_nat_true in Hmem; rewrite Hmem in *.
             rewrite Hcond in Hcondm.
             contradict Hcondm; auto.
Qed.

Theorem split_preserves_membership: forall m k t,
    member m t ->
    let '(l, _, _) := split k t in member m l \/
    let '(_, _, r) := split k t in member m r \/
    (m =? k) = true.
Proof.
  intros m k t; generalize m k; clear m k; induction t as [|l IHl n r IHr]; intros m k.
  - intros H; inversion H.
  - rewrite member_property_split; intros [Hmem|[Hmem|Hmem]]; simpl.
    * case_eq (Nat.compare k n); intros Heq.
      ** left; auto.
      ** pose proof (IHl m k Hmem); generalize H; clear H.
         case (split k l) as [[Hl Hn] Hr]; intros [H|[H|H]]; auto;
         right;left; apply left_member; auto.
      ** case (split k r) as [[Hl Hn] Hr]; left; apply left_member; auto.
    * case_eq (Nat.compare k n); intros Heq; auto.
      ** case (split k l) as [[Hl Hn] Hr]; right;left; apply right_member; auto.
      ** pose proof (IHr m k Hmem); generalize H; clear H. 
         case (split k r) as [[Hl Hn] Hr]; intros [H|[H|H]]; auto;
         left; apply right_member; auto.
    * case_eq (Nat.compare k n); intros Heq; auto.
      ** right; right; apply nat_compare_eq in Heq; rewrite Heq; auto.
      ** apply beq_nat_true in Hmem; case (split k l) as [[Hl Hn] Hr].
         rewrite Hmem in *; right; left; apply root_member.
      ** apply beq_nat_true in Hmem; case (split k r) as [[Hl Hn] Hr].
         rewrite Hmem in *; left; apply root_member.
Qed.

Theorem split_is_conservative_left: forall m k t,
    let '(l, _, _) := split k t in member m l -> member m t.
Proof.
  intros m k t; generalize m k; clear m k; induction t as [|l IHl n r IHr]; intros m k; simpl; auto.
  case_eq (Nat.compare k n); intros Heq.
  - intros Hmem; apply left_member; auto.
  - pose proof (IHl m k) as Hspl; generalize Hspl; clear Hspl.
    case (split k l) as [[Hl Hn] Hr]; intros Hmem Hv.
    apply left_member; apply Hmem; auto.
  - pose proof (IHr m k) as Hspl; generalize Hspl; clear Hspl.
    case (split k r) as [[Hl Hn] Hr]; intros Hfnl.
    rewrite member_property_split; intros [Hmem|[Hmem|Hmem]]; simpl.
    * apply left_member; auto.
    * apply right_member; apply Hfnl; auto.
    * apply beq_nat_true in Hmem; rewrite Hmem in *; apply root_member.
Qed.    
  
Theorem split_is_conservative_right: forall m k t,
    let '(_, _, r) := split k t in member m r -> member m t.
Proof.
  intros m k t; generalize m k; clear m k; induction t as [|l IHl n r IHr]; intros m k; simpl; auto.
  case_eq (Nat.compare k n); intros Heq.
  - intros Hmem; apply right_member; auto.
  - pose proof (IHl m k) as Hspl; generalize Hspl; clear Hspl.
    case (split k l) as [[Hl Hn] Hr]; intros Hfnl.
    rewrite member_property_split; intros [Hmem|[Hmem|Hmem]]; simpl.
    * apply left_member; apply Hfnl; auto.
    * apply right_member; auto.
    * apply beq_nat_true in Hmem; rewrite Hmem in *; apply root_member.
  - pose proof (IHr m k) as Hspl; generalize Hspl; clear Hspl.
    case (split k r) as [[Hl Hn] Hr]; intros Hmem Hv.
    apply right_member; apply Hmem; auto.
Qed.    

Theorem split_is_conservative_present: forall m t,
    let '(_, present, _) := split m t in present = true -> member m t.
Proof.
  intros m t; generalize m; clear m; induction t as [|l IHl n r IHr]; intros m; simpl; auto.
  - intros H; inversion H.
  - case_eq (Nat.compare m n); intros Heq.
    * intros _. apply nat_compare_eq in Heq; rewrite Heq; apply root_member.
    * pose proof (IHl m) as H; generalize H; clear H.
      case (split m l) as [[Hl Hn] Hr]; intros Hfnl Htr.
      apply left_member; apply Hfnl; auto.
    * pose proof (IHr m) as H; generalize H; clear H.
      case (split m r) as [[Hl Hn] Hr]; intros Hfnl Htr.
      apply right_member; apply Hfnl; auto.
Qed.    

Theorem split_is_sound_present: forall m t,
    let '(_, present, _) := split m t in tree_ordered t -> present = false -> ~ member m t.
Proof.
  intros m t; generalize m; clear m; induction t as [|l IHl n r IHr]; intros m; simpl; auto.
  - intros _ _ H; inversion H.
  - case_eq (Nat.compare m n); intros Heq.
    * intros _ Hf; inversion Hf.
    * pose proof (IHl m) as H; generalize H; clear H.
      case (split m l) as [[Hl Hn] Hr]; intros Hfnl Htr.
      pose proof (tree_ordered_decompose l n r Htr) as [Hlord [Hrord [Hltl Hltr]]].
      intros Hfl; pose proof (Hfnl Hlord Hfl) as Hneg; clear Hfnl Hfl.
      apply nat_compare_lt in Heq.
      rewrite member_property_split; intros [H|[H|H]].
      ++ apply Hneg; auto.
      ++ rewrite tree_more_lower_bound in Hltr; pose proof (Hltr m H); lia.
      ++ apply beq_nat_true in H; lia.
    * pose proof (IHr m) as H; generalize H; clear H.
      case (split m r) as [[Hl Hn] Hr]; intros Hfnl Htr.
      pose proof (tree_ordered_decompose l n r Htr) as [Hlord [Hrord [Hltl Hltr]]].
      intros Hfl; pose proof (Hfnl Hrord Hfl) as Hneg; clear Hfnl Hfl.
      apply nat_compare_gt in Heq.
      rewrite member_property_split; intros [H|[H|H]].
      ++ rewrite tree_less_upper_bound in Hltl; pose proof (Hltl m H); lia.
      ++ apply Hneg; auto.
      ++ apply beq_nat_true in H; lia.
Qed.    

Theorem union_main_property :
  forall n ta tb, member n ta \/ member n tb <-> member n (union ta tb).
Proof.
  intros n ta tb; split.
  - generalize n tb; clear n tb; induction ta as [| tl IHtl tn tr IHtr]; intros n tb; simpl.
    * case tb as [|tbl tbn tbr]; intros [H|H]; auto; inversion H.
    * case tb as [|tbl tbn tbr]; intros [H|H]; auto.
      ** inversion H.
      ** case (split tn (Fork tbl tbn tbr))  as [[lb _] lr].
         apply member_property_split in H; case H as [Hmem|[Hmem|Hmem]].
         *** apply left_member; apply IHtl; left; auto.
         *** apply right_member; apply IHtr; left; auto.
         *** apply beq_nat_true in Hmem; rewrite Hmem in *; apply root_member.
      ** pose proof (split_preserves_membership n tn (Fork tbl tbn tbr) H) as Hspl.
         generalize Hspl; clear Hspl.
         case_eq (split tn (Fork tbl tbn tbr)); intros [lb unused] lr Heq [Hm|[Hm|Hm]].
         *** apply left_member; apply IHtl; auto.
         *** apply right_member; apply IHtr; auto.
         *** apply beq_nat_true in Hm; rewrite Hm in *; apply root_member.
  - generalize n tb; clear n tb; induction ta as [| tl IHtl tn tr IHtr]; intros n tb; simpl.
    * case tb as [| tbl tbn tbr]; auto.
    * case tb as [| tbl tbn tbr]; auto.
      pose proof (split_is_conservative_left n tn (Fork tbl tbn tbr)) as Hspl; generalize Hspl; clear Hspl.
      pose proof (split_is_conservative_right n tn (Fork tbl tbn tbr)) as Hspl; generalize Hspl; clear Hspl.
      case (split tn (Fork tbl tbn tbr)) as [[lb unused] lr] eqn:Hspl; intros Hfnr Hfnl.
      rewrite member_property_split; intros [H|[H|H]].
      ** pose proof (IHtl n lb H) as [H1|H1].
         *** left; apply left_member; auto.
         *** right; apply Hfnl; auto.
      ** pose proof (IHtr n lr H) as [H1|H1].
         *** left; apply right_member; auto.
         *** right; apply Hfnr; auto.
      ** apply beq_nat_true in H; rewrite H in *; left; apply root_member.
Qed.        

Theorem split_tree_ordered_left : forall n t,
    tree_ordered t ->
    tree_less (let '(l, _, _) := split n t in l) n.
Proof.
  intros n t; generalize n; clear n.
  induction t as [| l IHl n r IHr ]; intros m Hord; simpl.
  - apply empty_tree_less.
  - case_eq (Nat.compare m n); intros Heq.
    * pose proof (tree_ordered_decompose l n r Hord) as [Hl [Hr [Hltl Hltr]]].
      apply nat_compare_eq in Heq; rewrite Heq; auto.
    * pose proof (IHl m) as H; generalize H; clear H.
      case (split m l) as [[Hll Hnl] Hrl]; intros Heqn; apply Heqn.
      pose proof (tree_ordered_decompose l n r Hord) as [Hl [Hr [Hltl Hltr]]].
      auto.
    * pose proof (IHr m) as H; generalize H; clear H.
      case (split m r) as [[Hll Hnl] Hrl]; intros Heqn.
      pose proof (tree_ordered_decompose l n r Hord) as [Hl [Hr [Hltl Hltr]]].
      apply fork_tree_less; try apply tree_less_upper_bound; try intros m' Hm'.
      ** rewrite tree_less_upper_bound in Hltl.
         pose proof (Hltl m' Hm').
         rewrite Nat.compare_gt_iff in Heq.
         eapply lt_trans; auto.
      ** pose proof (Heqn Hr) as Hltlm'.
         rewrite tree_less_upper_bound in Hltlm'.
         exact (Hltlm' m' Hm').
      ** apply Nat.compare_gt_iff; auto.
Qed.

Theorem split_tree_ordered_right : forall n t,
    tree_ordered t ->
    tree_more (let '(_, _, r) := split n t in r) n.
Proof.
  intros n t; generalize n; clear n.
  induction t as [| l IHl n r IHr ]; intros m Hord; simpl.
  - apply empty_tree_more.
  - case_eq (Nat.compare m n); intros Heq.
    * pose proof (tree_ordered_decompose l n r Hord) as [Hl [Hr [Hltl Hltr]]].
      apply nat_compare_eq in Heq; rewrite Heq; auto.
    * pose proof (IHl m) as H; generalize H; clear H.
      case (split m l) as [[Hll Hnl] Hrl]; intros Heqn.
      pose proof (tree_ordered_decompose l n r Hord) as [Hl [Hr [Hltl Hltr]]].
      apply fork_tree_more; try apply tree_more_lower_bound; try intros m' Hm'.
      ** pose proof (Heqn Hl) as Hltlm'.
         rewrite tree_more_lower_bound in Hltlm'.
         exact (Hltlm' m' Hm').
      ** rewrite tree_more_lower_bound in Hltr.
         pose proof (Hltr m' Hm').
         apply nat_compare_lt in Heq.
         eapply gt_trans; auto.
      ** apply Nat.compare_lt_iff; auto.
    * pose proof (IHr m) as H; generalize H; clear H.
      case (split m r) as [[Hll Hnl] Hrl]; intros Heqn; apply Heqn.
      pose proof (tree_ordered_decompose l n r Hord) as [Hl [Hr [Hltl Hltr]]].
      auto.
Qed.

Theorem split_tree_ordered_preserves_left : forall n t,
    tree_ordered t ->
    tree_ordered (let '(l, _, _) := split n t in l).
Proof.
  intros m t; induction t as [|l IHl n r IHr].
  - intros H; simpl; auto.
  - intros Hord; pose proof (tree_ordered_decompose l n r Hord) as [Hl [Hr [Hltl Hltr]]].
    simpl; case_eq (Nat.compare m n); intro Hcmp; auto.
    * pose proof (IHl Hl) as H; generalize H; clear H.
      case_eq (split m l); intros [ll lp] lr; simpl; auto.
    * pose proof (IHr Hr) as H; generalize H; clear H.
      case_eq (split m r); intros [ll lp] lr; simpl; intros Heq Hord'.
      apply tree_ordered_compose; repeat split; auto.
      apply tree_more_lower_bound; intros m' Hm'.
      rewrite tree_more_lower_bound in Hltr.
      apply Hltr.
      pose proof (split_is_conservative_left m' m r) as Himpl.
      rewrite Heq in Himpl; apply Himpl; auto.
Qed.
      
Theorem split_tree_ordered_preserves_right : forall n t,
    tree_ordered t ->
    tree_ordered (let '(_, _, r) := split n t in r).
Proof.
  intros m t; induction t as [|l IHl n r IHr].
  - intros H; simpl; auto.
  - intros Hord; pose proof (tree_ordered_decompose l n r Hord) as [Hl [Hr [Hltl Hltr]]].
    simpl; case_eq (Nat.compare m n); intro Hcmp; auto.
    * pose proof (IHl Hl) as H; generalize H; clear H.
      case_eq (split m l); intros [ll lp] lr; simpl; intros Heq Hord'.
      apply tree_ordered_compose; repeat split; auto.
      apply tree_less_upper_bound; intros m' Hm'.
      rewrite tree_less_upper_bound in Hltl.
      apply Hltl.
      pose proof (split_is_conservative_right m' m l) as Himpl.
      rewrite Heq in Himpl; apply Himpl; auto.
    * pose proof (IHr Hr) as H; generalize H; clear H.
      case_eq (split m r); intros [ll lp] lr; simpl; auto.
Qed.

Theorem intersection_conservative :
  forall n ta tb,
    tree_ordered ta -> tree_ordered tb ->
    member n (intersection ta tb) -> member n ta /\ member n tb.
Proof.
  intros n ta tb Hta Htb Htmem;
    generalize n Hta tb Htb Htmem;
    clear n tb Htb Hta Htmem.
  induction ta as [|tal IHtal tan tar IHtar].
  - simpl; intros n tord [|] _ H; inversion H.
  - intros n Hord.
    pose proof (tree_ordered_decompose tal tan tar Hord) as [Hl [Hr [Hltl Hltr]]].
    pose proof (IHtal n Hl) as IHl; clear IHtal.
    pose proof (IHtar n Hr) as IHr; clear IHtar.
    intros tb Hbord; simpl.
    pose proof (IHl tb Hbord) as IHlb.
    pose proof (IHr tb Hbord) as IHrb.
    generalize Hbord IHlb IHrb; clear Hbord IHlb IHrb.
    case tb as [|tbl tbn tbr]; simpl.
    * intros _ _ _ H; inversion H.
    * intros Hordb Hmeml Hmemr.
      pose proof (tree_ordered_decompose _ _ _ Hordb) as [Hl' [Hr' [Hltl' Hltr']]].
      case_eq (Nat.compare tan tbn); intros Heq.
      ** rewrite member_property_split.
         intros [Hmem'|[Hmem'|Hmem']].
         pose proof (IHl tbl Hl' Hmem') as [H1 H2]; split; apply left_member; auto.
         pose proof (IHr tbr Hr' Hmem') as [H1 H2]; split; apply right_member; auto.
         apply beq_nat_true in Hmem'; rewrite Hmem' in *.
         apply nat_compare_eq in Heq; rewrite Heq in *; split; apply root_member.
      ** case_eq (split tan tbl); intros [Htbl [|]] Htbr Heq'.
         rewrite member_property_split; intros [Hmem'|[Hmem'|Hmem']].
         *** pose proof (split_tree_ordered_preserves_left tan tbl Hl') as Htl.
             rewrite Heq' in Htl; pose proof (IHl Htbl Htl Hmem') as [H1 H2].
             split; first [apply left_member]; auto.
             pose proof (split_is_conservative_left n tan tbl) as H3.
             rewrite Heq' in H3; apply H3; auto.
         *** assert (tree_ordered (Fork Htbr tbn tbr)). {
             apply tree_ordered_compose; repeat split; auto.
             pose proof (split_tree_ordered_preserves_right tan tbl Hl') as Htl;
               rewrite Heq' in Htl; auto.
             apply tree_less_upper_bound; intros m Hmem.
             rewrite tree_less_upper_bound in Hltl'.
             apply Hltl'.
             pose proof (split_is_conservative_right m tan tbl) as H1; rewrite Heq' in H1.
             apply H1; auto.
           }
           pose proof (IHr _ H Hmem') as [H1 H2]; split.
             **** apply right_member; auto.
             **** rewrite member_property_split in H2; case H2 as [H2|[H2|H2]].
                  ***** pose proof (split_is_conservative_right n tan tbl) as H'; rewrite Heq' in H'; apply left_member; apply H'; auto. 
                  ***** apply right_member; auto.
                  ***** apply beq_nat_true in H2; rewrite H2 in *; apply root_member.
         *** apply beq_nat_true in Hmem'; rewrite Hmem' in *; split.
             **** apply root_member.
             **** pose proof (split_is_conservative_present tan tbl) as H.
                  rewrite Heq' in H; apply left_member; apply H; auto.
         *** intros Hmem; apply (member_property_concat_split) in Hmem.
             case Hmem as [Hmem|Hmem].
             **** assert (tree_ordered Htbl) as Htblord. {
                 pose proof (split_tree_ordered_preserves_left tan tbl Hl') as H'; rewrite Heq' in H'.
                 auto.
               }
               pose proof (IHl Htbl Htblord Hmem) as [H1 H2]; split.
                  apply left_member; auto.
                  pose proof (split_is_conservative_left n tan tbl) as H; rewrite Heq' in H.
                  apply left_member; apply H; auto.
             **** assert (tree_ordered (Fork Htbr tbn tbr)) as Htblord. {
                 apply tree_ordered_compose; repeat split; auto.
                 pose proof (split_tree_ordered_preserves_right tan tbl Hl') as H'; rewrite Heq' in H'; auto.
                 apply tree_less_upper_bound; intros m' Hmemm'.
                 rewrite tree_less_upper_bound in Hltl'; apply Hltl'.
                 pose proof (split_is_conservative_right m' tan tbl) as H; rewrite Heq' in H.
                 apply H; auto.
               }
               pose proof (IHr _ Htblord Hmem) as [H1 H2]; split.
                  apply right_member; auto.
                  rewrite member_property_split in H2; case H2 as [H|[H|H]].
                  ***** pose proof (split_is_conservative_right n tan tbl) as H'; rewrite Heq' in H'; apply left_member; apply H'; auto.
                  ***** apply right_member; auto.
                  ***** apply beq_nat_true in H; rewrite H in *; apply root_member.
      ** case_eq (split tan tbr); intros [Htbl [|]] Htbr Heq'.
         rewrite member_property_split; intros [Hmem'|[Hmem'|Hmem']].
         *** assert (tree_ordered (Fork tbl tbn Htbl)). {
             apply tree_ordered_compose; repeat split; auto.
             pose proof (split_tree_ordered_preserves_left tan tbr Hr') as Htl;
               rewrite Heq' in Htl; auto.
             apply tree_more_lower_bound; intros m Hmem.
             rewrite tree_more_lower_bound in Hltr'; apply Hltr'.
             pose proof (split_is_conservative_left m tan tbr) as H1; rewrite Heq' in H1.
             apply H1; auto.
           }
           pose proof (IHl _ H Hmem') as [H1 H2]; split.
             **** apply left_member; auto.
             **** rewrite member_property_split in H2; case H2 as [H2|[H2|H2]].
                  ***** apply left_member; auto.
                  ***** pose proof (split_is_conservative_left n tan tbr) as H'; rewrite Heq' in H'; apply right_member; apply H'; auto. 
                  ***** apply beq_nat_true in H2; rewrite H2 in *; apply root_member.
         *** pose proof (split_tree_ordered_preserves_right tan tbr Hr') as Htl.
             rewrite Heq' in Htl; pose proof (IHr Htbr Htl Hmem') as [H1 H2].
             split; first [apply right_member]; auto.
             pose proof (split_is_conservative_right n tan tbr) as H3.
             rewrite Heq' in H3; apply H3; auto.
         *** apply beq_nat_true in Hmem'; rewrite Hmem' in *; split.
             **** apply root_member.
             **** pose proof (split_is_conservative_present tan tbr) as H.
                  rewrite Heq' in H; apply right_member; apply H; auto.
         *** intros Hmem; apply (member_property_concat_split) in Hmem.
             case Hmem as [Hmem|Hmem].
             **** assert (tree_ordered (Fork tbl tbn Htbl)) as Htblord. {
                 apply tree_ordered_compose; repeat split; auto.
                 pose proof (split_tree_ordered_preserves_left tan tbr Hr') as H'; rewrite Heq' in H'; auto.
                 apply tree_more_lower_bound; intros m' Hmemm'.
                 rewrite tree_more_lower_bound in Hltr'; apply Hltr'.
                 pose proof (split_is_conservative_left m' tan tbr) as H; rewrite Heq' in H.
                 apply H; auto.
               }
               pose proof (IHl _ Htblord Hmem) as [H1 H2]; split.
                  apply left_member; auto.
                  rewrite member_property_split in H2; case H2 as [H|[H|H]].
                  ***** apply left_member; auto.
                  ***** pose proof (split_is_conservative_left n tan tbr) as H'; rewrite Heq' in H'; apply right_member; apply H'; auto.
                  ***** apply beq_nat_true in H; rewrite H in *; apply root_member.
             **** assert (tree_ordered Htbr) as Htblord. {
                 pose proof (split_tree_ordered_preserves_right tan tbr Hr') as H'; rewrite Heq' in H'.
                 auto.
               }
               pose proof (IHr Htbr Htblord Hmem) as [H1 H2]; split.
                  apply right_member; auto.
                  pose proof (split_is_conservative_right n tan tbr) as H; rewrite Heq' in H.
                  apply right_member; apply H; auto.        
Qed.

Theorem intersection_sound :
  forall n ta tb,
    tree_ordered ta -> tree_ordered tb ->
    member n ta /\ member n tb -> member n (intersection ta tb).
Proof.
  intros n ta tb Hta Htb [Htmem1 Htmem2];
    generalize n Hta tb Htb Htmem2 Htmem1;
    clear n tb Htb Hta Htmem1 Htmem2.
  induction ta as [|tal IHtal tan tar IHtar].
  - intros n _ tb _ _ H; inversion H.
  - intros n Hordf tb Hordtb Htb; rewrite member_property_split.
      pose proof (tree_ordered_decompose _ _ _ Hordf) as [Hfl [Hfr [Hfltl Hfltr]]].
    pose proof (IHtal n Hfl) as IHl; clear IHtal.
    pose proof (IHtar n Hfr) as IHr; clear IHtar.
    intros [Htal|[Htal|Htal]].
    * (* pose proof (IHl tb Hordtb Hmemtb Hmem) as H; generalize H; clear H; simpl. *)
      (* intros Hmemi; pose proof (intersection_conservative _ _ _ Hfl Hordtb Hmemi) as [Htal Htb]. *)
      destruct tb as[| tbl tbn tbr]; simpl; auto.
      case_eq (Nat.compare tan tbn); intros Hcomp.
      ** rewrite member_property_split in Htb; case Htb as [Htb|[Htb|Htb]].
         *** pose proof (tree_ordered_decompose _ _ _ Hordtb) as [Htbl [Htbr [Htbltl Htbltr]]].
             pose proof (IHl tbl Htbl Htb Htal); apply left_member; auto.
         *** pose proof (tree_ordered_decompose _ _ _ Hordtb) as [Htbl [Htbr [Htbltl Htbltr]]].
             rewrite tree_less_upper_bound in Hfltl.
             rewrite tree_more_lower_bound in Htbltr.
             pose proof (Hfltl n Htal) as H; generalize H; clear H.
             pose proof (Htbltr n Htb) as H; generalize H; clear H.
             apply nat_compare_eq in Hcomp; rewrite Hcomp in *; lia.
         *** apply nat_compare_eq in Hcomp; rewrite Hcomp in *.
             apply beq_nat_true in Htb; rewrite Htb in *; apply root_member.
      ** rewrite member_property_split in Htb; case Htb as [Htb|[Htb|Htb]].
         *** pose proof (split_preserves_membership n tan tbl Htb) as H; generalize H; clear H.
             case_eq (split tan tbl); intros [xl xp] xr Hspl.
             intros [Hmem'|[Hmem'|Hmem']].
             **** assert (tree_ordered xl) as Hord'. {
                 pose proof (tree_ordered_decompose _ _ _ Hordtb) as [Htbl [Htbr [Htbltl Htbltr]]].
                 pose proof (split_tree_ordered_preserves_left tan tbl Htbl) as H'; rewrite Hspl in H'; auto.
               }
               pose proof (IHl xl Hord' Hmem' Htal).
                  destruct xp.
                  apply left_member; auto.
                  apply concat_preserves_membership_left; auto.
             ****
               pose proof (tree_ordered_decompose _ _ _ Hordtb) as [Htbl [Htbr [Htbltl Htbltr]]].
               pose proof (split_tree_ordered_right tan tbl Htbl) as H; rewrite Hspl in H.
               apply nat_compare_lt in Hcomp.
               rewrite tree_less_upper_bound in Hfltl; pose proof (Hfltl n Htal).
               rewrite tree_more_lower_bound in H; pose proof (H n Hmem'); lia.
             **** apply beq_nat_true in Hmem'; rewrite <- Hmem' in *; clear Hmem' tan.
                  destruct xp; try apply root_member.
                  pose proof (tree_ordered_decompose _ _ _ Hordtb) as [Htbl [Htbr [Htbltl Htbltr]]].
                  pose proof (split_is_sound_present n tbl) as Htmp; rewrite Hspl in Htmp.
                  pose proof (Htmp Htbl eq_refl Htb) as [].
         *** pose proof (tree_ordered_decompose _ _ _ Hordtb) as [Htbl [Htbr [Htbltl Htbltr]]].
             apply nat_compare_lt in Hcomp.
             rewrite tree_less_upper_bound in Hfltl; pose proof (Hfltl n Htal).
             rewrite tree_more_lower_bound in Htbltr; pose proof (Htbltr n Htb).
             lia.
         *** apply nat_compare_lt in Hcomp.
             pose proof (tree_ordered_decompose _ _ _ Hordtb) as [Htbl [Htbr [Htbltl Htbltr]]].
             rewrite tree_less_upper_bound in Hfltl; pose proof (Hfltl n Htal).
             apply beq_nat_true in Htb.
             lia.
      ** rewrite member_property_split in Htb; case Htb as [Htb|[Htb|Htb]].
         *** case_eq (split tan tbr); intros [xl xp] xr Hspl.
             assert (tree_ordered (Fork tbl tbn xl)) as Hordfk. {
             pose proof (tree_ordered_decompose _ _ _ Hordtb) as [Htbl [Htbr [Htbltl Htbltr]]].
             apply tree_ordered_compose; repeat split; auto.
             pose proof (split_tree_ordered_preserves_left tan tbr Htbr) as H; rewrite Hspl in H; auto.
             pose proof (split_tree_ordered_right tan tbr Htbr) .
             apply tree_more_lower_bound; intros m Hm.
             pose proof (split_is_conservative_left m tan tbr) as H0; rewrite Hspl in H0.
             pose proof (H0 Hm) as H'; clear H0.
             rewrite tree_more_lower_bound in Htbltr; pose proof (Htbltr m H').
             auto.
           }
           pose proof (IHl (Fork tbl tbn xl) Hordfk (left_member _ _ _ _ Htb) Htal).
             destruct xp.
             apply left_member; auto.
             apply concat_preserves_membership_left; auto.
         *** pose proof (tree_ordered_decompose _ _ _ Hordtb) as [Htbl [Htbr [Htbltl Htbltr]]].
             pose proof (split_preserves_membership n tan tbr) as H; generalize H; clear H.
             case_eq (split tan tbr); intros [l n'] r Hspl Htmp.
             pose proof (Htmp Htb) as [H|[H|H]]; clear Htmp.
             **** assert (tree_ordered (Fork tbl tbn l)) as Hmemfk. {
                 apply tree_ordered_compose; repeat split; auto.
                 pose proof (split_tree_ordered_preserves_left tan tbr Htbr) as Htmp;
                   rewrite Hspl in Htmp; auto.
                 apply tree_more_lower_bound; intros m Hm.
                 rewrite tree_more_lower_bound in Htbltr; apply Htbltr.
                 pose proof (split_is_conservative_left m tan tbr) as H'; rewrite Hspl in H'; apply H'; auto.
               }
               pose proof (IHl (Fork tbl tbn l) Hmemfk (right_member _ _ _ _ H) Htal).
                  destruct n'; try (apply left_member); try (apply concat_preserves_membership_left); auto.
             **** pose proof (split_tree_ordered_right tan tbr Htbr) as H1; rewrite Hspl in H1.
                  rewrite tree_more_lower_bound in H1; pose proof (H1 n H).
                  rewrite tree_less_upper_bound in Hfltl; pose proof (Hfltl n Htal).
                  lia.
             **** apply beq_nat_true in H; rewrite <- H in *.
                  rewrite tree_less_upper_bound in Hfltl; pose proof (Hfltl n Htal).
                  lia.
         *** apply beq_nat_true in Htb; rewrite <- Htb in *; clear Htb.
             apply nat_compare_gt in Hcomp.
             (* pose proof (split_preserves_membership n tan tbr) as H; generalize H; clear H. *)
             case_eq (split tan tbr); intros [l present] r Hspl.
                  assert (tree_ordered (Fork tbl n l)) as H. {
                 pose proof (tree_ordered_decompose _ _ _ Hordtb) as [Htbl [Htbr [Htbltl Htbltr]]].
                 apply tree_ordered_compose; repeat split; auto.
                 pose proof (split_tree_ordered_preserves_left tan tbr Htbr) as Htmp;
                   rewrite Hspl in Htmp; auto.
                 apply tree_more_lower_bound; intros m Hm.
                 rewrite tree_more_lower_bound in Htbltr; apply Htbltr.
                 pose proof (split_is_conservative_left m tan tbr) as H; rewrite Hspl in H; apply H; auto.
           }
           pose proof (IHl (Fork tbl n l) H (root_member _ _ _) Htal) as Hcon.
           destruct present; try (apply left_member); try (apply concat_preserves_membership_left); auto.
    * destruct tb as[| tbl tbn tbr]; simpl; auto.
      case_eq (Nat.compare tan tbn); intros Hcomp.
      ** apply nat_compare_eq in Hcomp; rewrite Hcomp in *; clear Hcomp tan.
         pose proof (tree_ordered_decompose _ _ _ Hordtb) as [Htbl [Htbr [Htbltl Htbltr]]]; auto.
         rewrite member_property_split in Htb; case Htb as [Htb|[Htb|Htb]].
         *** rewrite tree_more_lower_bound in Hfltr; pose proof (Hfltr n Htal).
             rewrite tree_less_upper_bound in Htbltl; pose proof (Htbltl n Htb); lia.
         *** apply right_member; apply IHr; auto.
         *** apply beq_nat_true in Htb; rewrite Htb in *; apply root_member.
      ** apply nat_compare_lt in Hcomp.
         case_eq (split tan tbl); intros [l present] r Heq.
         pose proof (tree_ordered_decompose _ _ _ Hordtb) as [Htbl [Htbr [Htbltl Htbltr]]]; clear Hordtb; auto.
         rewrite member_property_split in Htb; case Htb as [Htb|[Htb|Htb]].
         *** assert (tree_ordered (Fork r tbn tbr)) as Hfkr. {
             apply tree_ordered_compose; repeat split; auto.
             pose proof (split_tree_ordered_preserves_right tan tbl Htbl) as Htmp; rewrite Heq in Htmp; auto.
             apply tree_less_upper_bound; intros m Hmemm.
             rewrite tree_less_upper_bound in Htbltl; apply Htbltl.
             pose proof (split_is_conservative_right m tan tbl) as H; rewrite Heq in H; apply H; auto.
           }
           assert (member n (Fork r tbn tbr)) as Hmemfk. {
             pose proof (split_preserves_membership n tan tbl Htb) as H; rewrite Heq in H.
             case H as [H|[H|H]].
             * pose proof (split_tree_ordered_left tan tbl Htbl) as H'; rewrite Heq in H'.
               rewrite tree_more_lower_bound in Hfltr; pose proof (Hfltr n Htal).
               rewrite tree_less_upper_bound in H'; pose proof (H' n H).
               lia.
             * apply left_member; auto.
             * apply beq_nat_true in H; rewrite <- H in *; clear H tan.
               rewrite tree_more_lower_bound in Hfltr; pose proof (Hfltr n Htal).
               lia.
           }
           pose proof (IHr _ Hfkr Hmemfk Htal).
             destruct present; try (apply right_member); try (apply concat_preserves_membership_right_strong); auto.
         *** generalize Htbltr; intros H1; rewrite tree_more_lower_bound in H1; pose proof (H1 n Htb) as Htbn; clear H1.
             generalize Hfltr; intros H1; rewrite tree_more_lower_bound in H1; pose proof (H1 n Htal) as Htan; clear H1.
             assert (tree_ordered (Fork r tbn tbr)) as Hfkr. {
             apply tree_ordered_compose; repeat split; auto.
             pose proof (split_tree_ordered_preserves_right tan tbl Htbl) as Htmp; rewrite Heq in Htmp; auto.
             apply tree_less_upper_bound; intros m Hmemm.
             rewrite tree_less_upper_bound in Htbltl; apply Htbltl.
             pose proof (split_is_conservative_right m tan tbl) as H; rewrite Heq in H; apply H; auto.
           }
           assert (member n (Fork r tbn tbr)) as Hmemfk. { apply right_member; auto. }
           pose proof (IHr _ Hfkr Hmemfk Htal).
             destruct present; try (apply right_member); try (apply concat_preserves_membership_right_strong); auto.
         *** apply beq_nat_true in Htb; rewrite <- Htb in *; clear Htb tbn.
             assert (tree_ordered (Fork r n tbr)) as Hfkr. {
             apply tree_ordered_compose; repeat split; auto.
             pose proof (split_tree_ordered_preserves_right tan tbl Htbl) as Htmp; rewrite Heq in Htmp; auto.
             apply tree_less_upper_bound; intros m Hmemm.
             rewrite tree_less_upper_bound in Htbltl; apply Htbltl.
             pose proof (split_is_conservative_right m tan tbl) as H; rewrite Heq in H; apply H; auto.
           }
           assert (member n (Fork r n tbr)) as Hmemfk. { apply root_member; auto. }
           pose proof (IHr _ Hfkr Hmemfk Htal).
             destruct present; try (apply right_member); try (apply concat_preserves_membership_right_strong); auto.
      ** apply nat_compare_gt in Hcomp.
         case_eq (split tan tbr); intros [l present] r Heq.
         pose proof (tree_ordered_decompose _ _ _ Hordtb) as [Htbl [Htbr [Htbltl Htbltr]]]; clear Hordtb; auto.
         generalize Hfltr; intros H1; rewrite tree_more_lower_bound in H1; pose proof (H1 n Htal) as Htan; clear H1.
         rewrite member_property_split in Htb; case Htb as [Htb|[Htb|Htb]].
         *** generalize Htbltl; intros H1; rewrite tree_less_upper_bound in H1; pose proof (H1 n Htb) as Htbn; clear H1.
             lia.
         *** generalize Htbltr; intros H1; rewrite tree_more_lower_bound in H1; pose proof (H1 n Htb) as Htbn; clear H1.
             assert (tree_ordered r) as Hrord.  {
             pose proof (split_tree_ordered_preserves_right tan tbr Htbr) as H; rewrite Heq in H; auto.
           }
           assert (member n r) as Hmem. {
             pose proof (split_preserves_membership n tan tbr Htb) as H; rewrite Heq in H.
             case H as [H|[H|H]]; auto.
             * pose proof (split_tree_ordered_left tan tbr Htbr) as H'; rewrite Heq in H'.
               rewrite tree_less_upper_bound in H'; pose proof (H' n H).
               lia.
             * apply beq_nat_true in H; rewrite <- H in *; clear H tan.
               rewrite tree_more_lower_bound in Hfltr; pose proof (Hfltr n Htal).
               lia.
           }
           pose proof (IHr _ Hrord Hmem Htal).
             destruct present; try (apply right_member); try (apply concat_preserves_membership_right_strong); auto.
         *** apply beq_nat_true in Htb; rewrite <- Htb in *; clear Htb tbn. lia.
    * apply beq_nat_true in Htal; rewrite <- Htal in *; clear Htal tan; simpl.
      destruct tb as[| tbl tbn tbr]; simpl; auto.
      case_eq (Nat.compare n tbn); intros Hcomp.
      ** apply root_member.
      ** case_eq (split n tbl); intros [l present] r Heq.
         destruct present; try (apply root_member).
         pose proof (tree_ordered_decompose _ _ _ Hordtb) as [Htbl [Htbr [Htbltl Htbltr]]]; clear Hordtb; auto.
         apply nat_compare_lt in Hcomp.
         rewrite member_property_split in Htb; case Htb as [Htb|[Htb|Htb]].
         *** pose proof (split_is_sound_present n tbl) as H0; rewrite Heq in H0.
             pose proof (H0 Htbl eq_refl Htb) as [].
         *** rewrite tree_more_lower_bound in Htbltr; pose proof (Htbltr n Htb); lia.
         *** apply beq_nat_true in Htb; rewrite <- Htb in *; clear Htb tbn; lia.
      ** case_eq (split n tbr); intros [l present] r Heq.
         destruct present; try (apply root_member).
         pose proof (tree_ordered_decompose _ _ _ Hordtb) as [Htbl [Htbr [Htbltl Htbltr]]]; clear Hordtb; auto.
         apply nat_compare_gt in Hcomp.
         rewrite member_property_split in Htb; case Htb as [Htb|[Htb|Htb]].
         *** rewrite tree_less_upper_bound in Htbltl; pose proof (Htbltl n Htb); lia.
         *** pose proof (split_is_sound_present n tbr) as H0; rewrite Heq in H0.
             pose proof (H0 Htbr eq_refl Htb) as [].
         *** apply beq_nat_true in Htb; rewrite <- Htb in *; clear Htb tbn; lia.
Qed.

Theorem intersection_main_property :
  forall n ta tb,
    tree_ordered ta -> tree_ordered tb ->
    member n ta /\ member n tb <-> member n (intersection ta tb).
Proof.
  intros n ta tb; split.
  apply intersection_sound; auto.
  apply intersection_conservative; auto.
Qed.
2 Likes
4

Should be Coq mentioned in the title too, since it’s used in the book?

1 Like
5

Maybe a more recent logo would be better? :grinning:

1 Like
6

Hello @Gopiandcode, do your research first, i am not as close to finish the book as you may think. I have a productivity problem (or i am simply an idiot). Anyway i am totally amazed by your hard work.

Not impossible. Note that OCaml was formerly Objective Caml and that makes some old books/tutorials harder to find. With Coq changing name too, i will be pretty conservative concerning the temporary book title.

The older one is shiny. I will not resist the pressure to align however.

1 Like
7

Sorry to be a little bit off-topic, but I wasn’t aware of this news and I can’t believe what I’ve read. Is it serious or do american students become totally crazy? I just hope that no french CS teacher will never be harassed or have problems just because they teach to their students that they will manipulate bits all along the day. In the same way that coq spells out as the slang word “cock” in english, in french the word “bit” spells out as the word “bite” which is the french slang word for “cock”. And you can find french programmers that do this silly joke : “pour avoir les deux bools, il suffit d’un bit”, which can both mean “to get the two bools, a bit is enough” or “to get the two balls, a cock is enough”.

I’m sorry but, from my point of view, I have difficulty to see this news as a way to be more inclusive or open to gender diversity, but it seems more as complete craziness or linguistic and cultural imperialism. :frowning_face:

4 Likes
8

I totally agree, it sounds much like an April fool.

9

A week late for an April fool. But the quest seems unattainable. With so many languages in the world it seems improbable that there is an acceptable short name in one language which is not a homophone of another with unfortunate connotations in another language.

So what are we saying: that it is unacceptable to have “difficult” homophones for English speakers, but OK to have one for those who speak, say, Swahili or Inuit? That sounds even worse as a work of cultural imperialism.

10

I have received this legitimate comment :

One may wonder what are the prerequisites for this book.

I think in terms of available copyleft material. So the best answer i can give is “read it if you understand the whole OCaml From the Ground Up book”. Obviously chapter 10 assumes you know what is a square matrix and how to add them. Chapter 5 is optional but assumes you know what is a group structure. More generally a decent math background is a great asset for programming.

Another legitimate comment is i write ocaml instead of OCaml. I don’t do it to belittle ocaml, i do it for not emphasize it too many times. Emphasizing it in the book title is enough for me.

11

On language usage, the title “Algorhythmic with Ocaml” isn’t quite right. The English equivalent of “algorhythmique” in this sense is “algorhythmics”, or more verbosely “the study of algorhythms”.

However, the scope of the book seems wider than just the study of algorhythms. It seems in part intended as a more advanced language tutorial for those who already have a basic understanding of the language.

2 Likes
12

Right. My English dictionary tells me the correct word is algorithmics, not “algorhythmics”, thus the new title becomes “Algorithmics with OCaml”. Note that the changes i apply are local only, nothing changes from your point of view.

Indeed the intended audience is people wanting to push beyond the 'a List.t routines.

13

Yes you are right about the spelling. I think there is a definite need for a book like this going beyond the usual beginners’ texts, so I think this is great.

As far as concerns 'a List.t, I was pleased to see that, for example, you will be covering things like the universal quantification of type variables. Having been told in a beginners’ text that ocaml’s parametric polymorphism is similar to generics in Java or C++, beginners are left to puzzle over why the element type of a container is represented by a type variable in 'a List.t (and in corresponding functions which can be applied to the list) whereas in a set it is represented by the Set.OrderedType.t/Set.S.elt type; or why you can write a partial i/o function template <class T> void print(T) in C++, whereas it is I think impossible to write a function val print : 'a -> unit in ocaml without resorting to the C FFI and throwing exceptions for unimplemented types (compare the polymorphic comparison operator with that).

2 Likes
14

It’s great to see a new book on Ocaml, thanks for this. I have an aside question, more general than this book. So maybe it doesn’t fit this thread, sorry. It concerns Chapter 2 “Algebraic datatypes”. I’ve always found the terminology “algebraic datatype” confusing (and pedantic). To be short, my impression is that it only frightens newcomers – for nothing.

It’s difficult to find a precise definition outside of the ocaml world. Maybe even inside. I thought every type composed of several “basic” type was “algebraic”. This includes products (tuples) and sums (unions).

Chapter 2 starts with Float, which conveys the idea that its an algebraic datatype. Then pairs; OK they are “algebraic”. Then “enumerated type”. But then there is a subsection 2.12 that says that algebraic datatypes (ADT) are only “enumerations of tuples”. Is this true?
On the one hand it implies that, finally, a pair is not really an ADT (or a degenerate one). On the other hand, why not allow more general enumerations (for instance unions of unions, etc.)

I find this confusing. All in all, why not ban the terminology “algebraic datatype” altogether ? :wink:

15

These kinds of “lets hide how things are to newcomers” tend to end up being unproductive for them.

Using the terms that are used in the trade is a better idea, e.g. soon enough the newcomer will for example hit the term GADT at which point knowing what ADT stands for (abstract data type right ? :joy:) will be useful.

Not saying better terminology could be used/found but then you somehow need the environment (manuals, API docs, community, etc) to follow suit.

1 Like
16

float is not an algebraic datatype.
a record type maybe composed of several “basic” types but is not an algebraic datatype. it’s a product type.
a pair is not an algebraic datatype. it’s a product type.
an abstract data type is a vocabulary from class-oriented programming, it’s not the same thing as an algebraic datatype.
an enumeration is a sum type.
an enumeration of tuple types is a sum of products type which is exactly what an algebraic datatype is supposed to be (some tuple eventually can be empty).
an inductive datatype is a recursive algebraic datatype.

I know this does not sound beginner-friendly (just like variable being immutable by default) yet it’s the way ocaml & haskell have to be learned.

17

this is not what the wikipedia entry states, though, Algebraic data type - Wikipedia :
" Two common classes of algebraic types are product types (i.e., tuples and records) and sum types"

18

I believe wikipedia means that two common components of algebraic types are product types and sum types.

19

Technically, algebraic types aren’t constrained to just these types, for example quotient types are also possible. They are just rarely implemented anywhere. The Wikipedia article fails to explain the core idea behind these types, IMHO. While explanation of the functors and monads often involves basic concepts of homomorphism and category theory, algebraic types aren’t explained this way. I think, it should have been done.

https://www.hedonisticlearning.com/posts/quotient-types-for-programmers.html

20

In fact, I don’t want to hide the truth, I’d rather remove terms that (to me) are hiding it, because they are not well defined.

Of course, as you said, it’s already “in the trade”, I’m not going to remove anything myself ;). But hey, just chatting :wink:

1 Like