Add new fold_ind induction principle for folds

fold_inv is in Type, hence can prove goals such as `{ x | P x }`.
Also, no extensionality property is needed.

fold_rec is now derived from fold_inv.

1 files changed, 82 insertions, 63 deletions

diff --git a/lib/Maps.v b/lib/Maps.v
index 54d92897..092ab6ea 100644
--- a/lib/Maps.v
+++ b/lib/Maps.v
@@ -1285,103 +1285,122 @@ Module ZTree := ITree(ZIndexed).
 
 Module Tree_Properties(T: TREE).
 
-(** An induction principle over [fold]. *)
+(** Two induction principles over [fold]. *)
 
 Section TREE_FOLD_IND.
 
 Variables V A: Type.
 Variable f: A -> T.elt -> V -> A.
-Variable P: T.t V -> A -> Prop.
+Variable P: T.t V -> A -> Type.
 Variable init: A.
 Variable m_final: T.t V.
 
-Hypothesis P_compat:
-  forall m m' a,
-  (forall x, T.get x m = T.get x m') ->
-  P m a -> P m' a.
-
 Hypothesis H_base:
-  P (T.empty _) init.
+  forall m,
+  (forall k, T.get k m = None) ->
+  P m init.
 
 Hypothesis H_rec:
   forall m a k v,
-  T.get k m = None -> T.get k m_final = Some v -> P m a -> P (T.set k v m) (f a k v).
+  T.get k m = Some v -> T.get k m_final = Some v ->
+  P (T.remove k m) a -> P m (f a k v).
 
-Let f' (a: A) (p : T.elt * V) := f a (fst p) (snd p).
+Let f' (p : T.elt * V) (a: A) := f a (fst p) (snd p).
 
-Let P' (l: list (T.elt * V)) (a: A) : Prop :=
-  forall m, list_equiv l (T.elements m) -> P m a.
+Let P' (l: list (T.elt * V)) (a: A) : Type :=
+  forall m, (forall k v, In (k, v) l <-> T.get k m = Some v) -> P m a.
 
-Remark H_base':
+Let H_base':
   P' nil init.
 Proof.
-  red; intros. apply P_compat with (T.empty _); auto.
-  intros. rewrite T.gempty. symmetry. case_eq (T.get x m); intros; auto.
-  assert (In (x, v) nil). rewrite (H (x, v)). apply T.elements_correct. auto.
-  contradiction.
+  intros m EQV. apply H_base.
+  intros. destruct (T.get k m) as [v|] eqn:G; auto.
+  apply EQV in G. contradiction.
 Qed.
 
-Remark H_rec':
+Let H_rec':
   forall k v l a,
-  ~In k (List.map (@fst T.elt V) l) ->
-  In (k, v) (T.elements m_final) ->
+  ~In k (List.map fst l) ->
+  T.get k m_final = Some v ->
   P' l a ->
-  P' (l ++ (k, v) :: nil) (f a k v).
+  P' ((k, v) :: l) (f a k v).
 Proof.
-  unfold P'; intros.
+  unfold P'; intros k v l a NOTIN FINAL HR m EQV.
   set (m0 := T.remove k m).
-  apply P_compat with (T.set k v m0).
-    intros. unfold m0. rewrite T.gsspec. destruct (T.elt_eq x k).
-    symmetry. apply T.elements_complete. rewrite <- (H2 (x, v)).
-    apply in_or_app. simpl. intuition congruence.
-    apply T.gro. auto.
-  apply H_rec. unfold m0. apply T.grs. apply T.elements_complete. auto.
-  apply H1. red. intros [k' v'].
-  split; intros.
-  apply T.elements_correct. unfold m0. rewrite T.gro. apply T.elements_complete.
-  rewrite <- (H2 (k', v')). apply in_or_app. auto.
-  red; intro; subst k'. elim H. change k with (fst (k, v')). apply in_map. auto.
-  assert (T.get k' m0 = Some v'). apply T.elements_complete. auto.
-  unfold m0 in H4. rewrite T.grspec in H4. destruct (T.elt_eq k' k). congruence.
-  assert (In (k', v') (T.elements m)). apply T.elements_correct; auto.
-  rewrite <- (H2 (k', v')) in H5. destruct (in_app_or _ _ _ H5). auto.
-  simpl in H6. intuition congruence.
+  apply H_rec.
+- apply EQV. simpl; auto.
+- auto.
+- apply HR. intros k' v'. rewrite T.grspec. split; intros; destruct (T.elt_eq k' k).
+  + subst k'. elim NOTIN. change k with (fst (k, v')). apply List.in_map; auto.
+  + apply EQV. simpl; auto.
+  + congruence.
+  + apply EQV in H. simpl in H. intuition congruence.
 Qed.
 
-Lemma fold_rec_aux:
-  forall l1 l2 a,
-  list_equiv (l2 ++ l1) (T.elements m_final) ->
-  list_disjoint (List.map (@fst T.elt V) l1) (List.map (@fst T.elt V) l2) ->
-  list_norepet (List.map (@fst T.elt V) l1) ->
-  P' l2 a -> P' (l2 ++ l1) (List.fold_left f' l1 a).
+Lemma fold_ind_aux:
+  forall l,
+  (forall k v, In (k, v) l -> T.get k m_final = Some v) ->
+  list_norepet (List.map fst l) ->
+  P' l (List.fold_right f' init l).
 Proof.
-  induction l1; intros; simpl.
-  rewrite <- List.app_nil_end. auto.
-  destruct a as [k v]; simpl in *. inv H1.
-  change ((k, v) :: l1) with (((k, v) :: nil) ++ l1). rewrite <- List.app_ass. apply IHl1.
-  rewrite app_ass. auto.
-  red; intros. rewrite map_app in H3. destruct (in_app_or _ _ _ H3). apply H0; auto with coqlib.
-  simpl in H4. intuition congruence.
-  auto.
-  unfold f'. simpl. apply H_rec'; auto. eapply list_disjoint_notin; eauto with coqlib.
-  rewrite <- (H (k, v)). apply in_or_app. simpl. auto.
+  induction l as [ | [k v] l ]; simpl; intros FINAL NOREPET.
+- apply H_base'.
+- apply H_rec'.
+  + inv NOREPET. auto.
+  + apply FINAL. auto.
+  + apply IHl. auto. inv NOREPET; auto.
 Qed.
 
-Theorem fold_rec:
+Theorem fold_ind:
   P m_final (T.fold f m_final init).
 Proof.
-  intros. rewrite T.fold_spec. fold f'.
-  assert (P' (nil ++ T.elements m_final) (List.fold_left f' (T.elements m_final) init)).
-    apply fold_rec_aux.
-    simpl. red; intros; tauto.
-    simpl. red; intros. elim H0.
-    apply T.elements_keys_norepet.
-    apply H_base'.
-  simpl in H. red in H. apply H. red; intros. tauto.
+  intros.
+  set (l' := List.rev (T.elements m_final)).
+  assert (P' l' (List.fold_right f' init l')).
+  { apply fold_ind_aux.
+    intros. apply T.elements_complete. apply List.in_rev. auto.
+    unfold l'; rewrite List.map_rev. apply list_norepet_rev. apply T.elements_keys_norepet. }
+  unfold l', f' in X; rewrite fold_left_rev_right in X.
+  rewrite T.fold_spec. apply X.
+  intros; simpl. rewrite <- List.in_rev.
+  split. apply T.elements_complete. apply T.elements_correct.
 Qed.
 
 End TREE_FOLD_IND.
 
+Section TREE_FOLD_REC.
+
+Variables V A: Type.
+Variable f: A -> T.elt -> V -> A.
+Variable P: T.t V -> A -> Prop.
+Variable init: A.
+Variable m_final: T.t V.
+
+Hypothesis P_compat:
+  forall m m' a,
+  (forall x, T.get x m = T.get x m') ->
+  P m a -> P m' a.
+
+Hypothesis H_base:
+  P (T.empty _) init.
+
+Hypothesis H_rec:
+  forall m a k v,
+  T.get k m = None -> T.get k m_final = Some v -> P m a -> P (T.set k v m) (f a k v).
+
+Theorem fold_rec:
+  P m_final (T.fold f m_final init).
+Proof.
+  apply fold_ind. 
+- intros. apply P_compat with (T.empty V); auto.
+  + intros. rewrite T.gempty. auto.
+- intros. apply P_compat with (T.set k v (T.remove k m)).
+  + intros. rewrite T.gsspec, T.grspec. destruct (T.elt_eq x k); auto. congruence.
+  + apply H_rec; auto. apply T.grs.
+Qed.
+
+End TREE_FOLD_REC.
+
 (** A nonnegative measure over trees *)
 
 Section MEASURE.