From 2ae43be7b9d4118335c9d2cef6e098f9b9f807fe Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Thu, 9 Feb 2006 14:55:48 +0000
Subject: Initial import of compcert

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 lib/Inclusion.v | 367 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 367 insertions(+)
 create mode 100644 lib/Inclusion.v

(limited to 'lib/Inclusion.v')

diff --git a/lib/Inclusion.v b/lib/Inclusion.v
new file mode 100644
index 00000000..1df7517f
--- /dev/null
+++ b/lib/Inclusion.v
@@ -0,0 +1,367 @@
+(** Tactics to reason about list inclusion. *)
+
+(** This file (contributed by Laurence Rideau) defines a tactic [in_tac]
+  to reason over list inclusion.  It expects goals of the following form:
+<<
+  id : In x l1
+  ============================
+     In x l2
+>>
+and succeeds if it can prove that [l1] is included in [l2].  
+The lists [l1] and [l2] must belong to the following sub-language [L]
+<<
+  L ::= L++L | E | E::L
+>>
+The tactic uses no extra fact.
+
+A second tactic, [incl_tac], handles goals of the form
+<<
+  =============================
+    incl l1 l2
+>>
+*)
+
+Require Import List.
+Require Import ArithRing.
+
+Ltac all_app e :=
+  match e with
+  | cons ?x nil => constr:(cons x nil)
+  | cons ?x ?tl => 
+      let v := all_app tl in constr:(app (cons x nil) v)
+  | app ?e1 ?e2 =>
+    let v1 := all_app e1 with v2 := all_app e2 in
+    constr:(app v1 v2)
+  | _ => e
+  end.
+
+(** This data type, [flatten], [insert_bin], [sort_bin] and a few theorem
+  are taken from the CoqArt book, chapt. 16. *)
+
+Inductive bin : Set := node : bin->bin->bin | leaf : nat->bin.
+
+Fixpoint flatten_aux (t fin:bin){struct t} : bin :=
+  match t with
+  | node t1 t2 => flatten_aux t1 (flatten_aux t2 fin)
+  | x => node x fin
+  end.
+
+Fixpoint flatten (t:bin) : bin :=
+  match t with
+  | node t1 t2 => flatten_aux t1 (flatten t2)
+  | x => x
+  end.
+
+Fixpoint nat_le_bool (n m:nat){struct m} : bool :=
+  match n, m with
+  | O, _ => true
+  | S _, O => false
+  | S n, S m => nat_le_bool n m
+  end.
+
+Fixpoint insert_bin (n:nat)(t:bin){struct t} : bin :=
+  match t with
+  | leaf m => 
+    if nat_le_bool n m then
+       node (leaf n)(leaf m)
+    else
+       node (leaf m)(leaf n)
+  | node (leaf m) t' =>
+    if nat_le_bool n m then node (leaf n) t else node (leaf m)(insert_bin n t')
+  | t => node (leaf n) t
+  end.
+
+Fixpoint sort_bin (t:bin) : bin :=
+  match t with
+  | node (leaf n) t' => insert_bin n (sort_bin t')
+  | t => t
+  end.
+
+Section assoc_eq.
+ Variables (A : Set)(f : A->A->A).
+ Hypothesis assoc : forall x y z:A, f x (f y z) = f (f x y) z.
+
+ Fixpoint bin_A (l:list A)(def:A)(t:bin){struct t} : A :=
+   match t with
+   | node t1 t2 => f (bin_A l def t1)(bin_A l def t2)
+   | leaf n => nth n l def
+   end.
+
+ Theorem flatten_aux_valid_A :
+  forall (l:list A)(def:A)(t t':bin),
+   f (bin_A l def t)(bin_A l def t') = bin_A l def (flatten_aux t t').
+ Proof.
+  intros l def t; elim t; simpl; auto.
+  intros t1 IHt1 t2 IHt2 t';  rewrite <- IHt1; rewrite <- IHt2.
+  symmetry; apply assoc.
+ Qed.
+
+ Theorem flatten_valid_A :
+  forall (l:list A)(def:A)(t:bin),
+    bin_A l def t = bin_A l def (flatten t).
+ Proof.
+  intros l def t; elim t; simpl; trivial.
+  intros t1 IHt1 t2 IHt2; rewrite <- flatten_aux_valid_A; rewrite <- IHt2.
+  trivial.
+ Qed.
+
+End assoc_eq.
+
+Ltac compute_rank l n v :=
+  match l with
+  | (cons ?X1 ?X2) =>
+    let tl := constr:X2 in
+    match constr:(X1 = v) with
+    | (?X1 = ?X1) => n
+    | _ => compute_rank tl (S n) v
+    end
+  end.
+
+Ltac term_list_app l v :=
+  match v with
+  | (app ?X1 ?X2) =>
+    let l1 := term_list_app l X2 in term_list_app l1 X1
+  | ?X1 => constr:(cons X1 l)
+  end.
+
+Ltac model_aux_app l v :=
+  match v with
+  | (app ?X1 ?X2) =>
+    let r1 := model_aux_app l X1 with r2 := model_aux_app l X2 in
+      constr:(node r1 r2)
+  | ?X1 => let n := compute_rank l 0 X1 in constr:(leaf n)
+  | _ => constr:(leaf 0)
+  end.
+
+Theorem In_permute_app_head :
+  forall A:Set, forall r:A, forall x y l:list A,
+   In r (x++y++l) -> In r (y++x++l).
+intros A r x y l; generalize r; change (incl (x++y++l)(y++x++l)).
+repeat rewrite ass_app; auto with datatypes.
+Qed.
+
+Theorem insert_bin_included : 
+  forall x:nat, forall t2:bin,
+  forall (A:Set) (r:A) (l:list (list A))(def:list A), 
+     In r (bin_A (list A) (app (A:=A)) l def (insert_bin x t2)) ->
+     In r (bin_A (list A) (app (A:=A)) l def (node (leaf x) t2)).
+intros x t2; induction t2.
+intros A r l def.
+destruct t2_1 as [t2_11 t2_12|y].
+simpl.
+repeat rewrite app_ass.
+auto.
+simpl; repeat rewrite app_ass.
+simpl; case (nat_le_bool x y); simpl.
+auto.
+intros H; apply In_permute_app_head.
+elim in_app_or with (1:= H); clear H; intros H.
+apply in_or_app; left; assumption.
+apply in_or_app; right;apply (IHt2_2 A r l);assumption.
+intros A r l def; simpl.
+case (nat_le_bool x n); simpl.
+auto.
+intros H.
+rewrite (app_nil_end (nth x l def)) in H.
+rewrite (app_nil_end (nth n l def)).
+apply In_permute_app_head; assumption.
+Qed.
+
+Theorem in_or_insert_bin :
+  forall (n:nat) (t2:bin) (A:Set)(r:A)(l:list (list A)) (def:list A),
+  In r (nth n l def) \/ In r (bin_A (list A)(app (A:=A)) l def t2) ->
+  In r (bin_A (list A)(app (A:=A)) l def (insert_bin n t2)).
+intros n t2 A r l def; induction t2.
+destruct t2_1 as [t2_11 t2_12| y].
+simpl; apply in_or_app.
+simpl; case (nat_le_bool n y); simpl.
+intros H.
+apply in_or_app.
+exact H.
+intros [H|H].
+apply in_or_app; right; apply IHt2_2; auto.
+elim in_app_or with (1:= H);clear H; intros H; apply in_or_app; auto.
+simpl; intros [H|H]; case (nat_le_bool n n0); simpl; apply in_or_app; auto.
+Qed.
+
+Theorem sort_included :
+  forall t:bin, forall (A:Set)(r:A)(l:list(list A))(def:list A),
+    In r (bin_A (list A) (app (A:=A)) l def (sort_bin t)) ->
+    In r (bin_A (list A) (app (A:=A)) l def t).
+induction t.
+destruct t1.
+simpl;intros; assumption.
+intros A r l def H; simpl in H; apply insert_bin_included.
+generalize (insert_bin_included _ _ _ _ _ _ H); clear H; intros H.
+simpl in H.
+elim in_app_or with (1 := H);clear H; intros H;
+apply in_or_insert_bin; auto.
+simpl;intros;assumption.
+Qed.
+
+Theorem sort_included2 :
+  forall t:bin, forall (A:Set)(r:A)(l:list(list A))(def:list A),
+    In r (bin_A (list A) (app (A:=A)) l def t) ->
+    In r (bin_A (list A) (app (A:=A)) l def (sort_bin t)).
+induction t.
+destruct t1.
+simpl; intros; assumption.
+intros A r l def H; simpl in H.
+simpl; apply in_or_insert_bin.
+elim in_app_or with (1:= H); auto.
+simpl; auto.
+Qed.
+
+Theorem in_remove_head :
+  forall (A:Set)(x:A)(l1 l2 l3:list A),
+  In x (l1++l2) -> (In x l2 -> In x l3) -> In x (l1++l3).
+intros A x l1 l2 l3 H H1.
+elim in_app_or with (1:= H);clear H; intros H; apply in_or_app; auto.
+Qed.
+
+Fixpoint check_all_leaves (n:nat)(t:bin) {struct t} : bool :=
+  match t with
+    leaf n1 => nateq n n1
+  | node t1 t2 => andb (check_all_leaves n t1)(check_all_leaves n t2)
+  end.
+
+Fixpoint remove_all_leaves (n:nat)(t:bin){struct t} : bin :=
+  match t with
+    leaf n => leaf n
+  | node (leaf n1) t2 =>
+    if nateq n n1 then remove_all_leaves n t2 else t
+  | _ => t
+  end.
+
+Fixpoint test_inclusion (t1 t2:bin) {struct t1} : bool :=
+  match t1 with
+    leaf n => check_all_leaves n t2
+  | node (leaf n1) t1' =>
+     check_all_leaves n1 t2 || test_inclusion t1' (remove_all_leaves n1 t2)
+  | _ => false
+  end.
+
+Theorem check_all_leaves_sound :
+  forall x t2,
+    check_all_leaves x t2 = true ->
+    forall (A:Set)(r:A)(l:list(list A))(def:list A),
+    In r (bin_A (list A) (app (A:=A)) l def t2) ->
+    In r (nth x l def).
+intros x t2; induction t2; simpl.
+destruct (check_all_leaves x t2_1);
+destruct (check_all_leaves x t2_2); simpl; intros Heq; try discriminate.
+intros A r l def H; elim in_app_or with (1:= H); clear H; intros H; auto.
+intros Heq A r l def; rewrite (nateq_prop x n); auto.
+rewrite Heq; unfold Is_true; auto.
+Qed.
+
+Theorem remove_all_leaves_sound :
+  forall x t2,
+  forall (A:Set)(r:A)(l:list(list A))(def:list A),
+  In r (bin_A (list A) (app(A:=A)) l def t2) ->
+  In r (bin_A (list A) (app(A:=A)) l def (remove_all_leaves x t2)) \/
+  In r (nth x l def).
+intros x t2; induction t2; simpl.
+destruct t2_1.
+simpl; auto.
+intros A r l def.
+generalize (refl_equal (nateq x n)); pattern (nateq x n) at -1;
+ case (nateq x n); simpl; auto.
+intros Heq_nateq.
+assert (Heq_xn : x=n).
+apply nateq_prop; rewrite Heq_nateq;unfold Is_true;auto.
+rewrite Heq_xn.
+intros H; elim in_app_or with (1:= H); auto.
+clear H; intros H.
+rewrite Heq_xn in IHt2_2; auto.
+auto.
+Qed.
+
+Theorem test_inclusion_sound :
+  forall t1 t2:bin,
+  test_inclusion t1 t2 = true ->
+  forall (A:Set)(r:A)(l:list(list A))(def:list A),
+  In r (bin_A (list A)(app(A:=A)) l def t2) ->
+  In r (bin_A (list A)(app(A:=A)) l def t1).
+intros t1; induction t1.
+destruct t1_1 as [t1_11 t1_12|x].
+simpl; intros; discriminate.
+simpl; intros t2 Heq A r l def H.
+assert 
+ (check_all_leaves x t2 = true \/ 
+  test_inclusion t1_2 (remove_all_leaves x t2) = true).
+destruct (check_all_leaves x t2);
+destruct (test_inclusion t1_2 (remove_all_leaves x t2));
+simpl in Heq; try discriminate Heq; auto.
+elim H0; clear H0; intros H0.
+apply in_or_app; left; apply check_all_leaves_sound with (1:= H0); auto.
+elim remove_all_leaves_sound with (x:=x)(1:= H); intros H'.
+apply in_or_app; right; apply IHt1_2 with (1:= H0); auto.
+apply in_or_app; auto.
+simpl; apply check_all_leaves_sound.
+Qed.
+
+Theorem inclusion_theorem :
+  forall t1 t2 : bin,
+    test_inclusion (sort_bin (flatten t1)) (sort_bin (flatten t2)) = true ->
+    forall (A:Set)(r:A)(l:list(list A))(def:list A),
+    In r (bin_A (list A) (app(A:=A)) l def t2) ->
+    In r (bin_A (list A) (app(A:=A)) l def t1).
+intros t1 t2 Heq A r l def H.
+rewrite flatten_valid_A with (t:= t1)(1:= (ass_app (A:= A))).
+apply sort_included.
+apply test_inclusion_sound with (t2 := sort_bin (flatten t2)).
+assumption.
+apply sort_included2.
+rewrite <- flatten_valid_A with (1:= (ass_app (A:= A))).
+assumption.
+Qed.
+
+Ltac in_tac :=
+  match goal with
+  | id : In ?x nil |- _ => elim id
+  | id : In ?x ?l1 |- In ?x ?l2 =>
+    let t := type of x in
+    let v1 := all_app l1 in
+    let v2 := all_app l2 in
+    (let l := term_list_app (nil (A:=list t)) v2 in
+     let term1 := model_aux_app l v1 with
+         term2 := model_aux_app l v2 in
+        (change (In x (bin_A (list t) (app(A:=t)) l (nil(A:=t)) term2));
+        apply inclusion_theorem with (t2:= term1);[apply refl_equal|exact id]))
+  end.
+
+Ltac incl_tac :=
+  match goal with
+  |- incl _ _ => intro; intro; in_tac
+  end.
+   
+(* Usage examples.
+
+Theorem ex1 : forall x y z:nat, forall l1 l2 : list nat,
+   In x (y::l1++l2) -> In x (l2++z::l1++(y::nil)).
+intros.
+in_tac.
+Qed.
+
+Fixpoint mklist (f:nat->nat)(n:nat){struct n} : list nat :=
+ match n with 0 => nil | S p => mklist f p++(f p::nil) end.
+
+(* At the time of writing these lines, this example takes about 5 seconds
+     for 40 elements and 22 seconds for 60 elements.
+   A variant to the example is to replace mklist f p++(f p::nil) with
+   f p::mklist f p, in this case the time is 6 seconds for 40 elements and
+   35 seconds for 60 elements. *)
+
+Theorem ex2 : 
+  forall x : nat, In x (mklist (fun y => y) 40) ->
+     In x (mklist (fun y => (40 - 1) - y) 40).
+lazy beta iota zeta delta [mklist minus].
+intros.
+in_tac.
+Qed.
+
+(* The tactic could be made more efficient by using binary trees and
+   numbers of type positive instead of lists and natural numbers. *)
+
+*)
-- 
cgit