From 8018e923c75eb5504310864f821972f794b7d554 Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Wed, 13 Feb 2019 20:40:51 -0500 Subject: New upstream version 8.8.0+1.gbp069dc3b --- theories/AAC.v | 901 +++++++++++++++++++++++++++++++++++++++++++++++++++ theories/Caveats.v | 376 +++++++++++++++++++++ theories/Instances.v | 261 +++++++++++++++ theories/Tutorial.v | 401 +++++++++++++++++++++++ theories/Utils.v | 257 +++++++++++++++ 5 files changed, 2196 insertions(+) create mode 100644 theories/AAC.v create mode 100644 theories/Caveats.v create mode 100644 theories/Instances.v create mode 100644 theories/Tutorial.v create mode 100644 theories/Utils.v (limited to 'theories') diff --git a/theories/AAC.v b/theories/AAC.v new file mode 100644 index 0000000..d7cc7a2 --- /dev/null +++ b/theories/AAC.v @@ -0,0 +1,901 @@ +(***************************************************************************) +(* This is part of aac_tactics, it is distributed under the terms of the *) +(* GNU Lesser General Public License version 3 *) +(* (see file LICENSE for more details) *) +(* *) +(* Copyright 2009-2010: Thomas Braibant, Damien Pous. *) +(***************************************************************************) + +(** * Theory file for the aac_rewrite tactic + + We define several base classes to package associative and possibly + commutative operators, and define a data-type for reified (or + quoted) expressions (with morphisms). + + We then define a reflexive decision procedure to decide the + equality of reified terms: first normalise reified terms, then + compare them. This allows us to close transitivity steps + automatically, in the [aac_rewrite] tactic. + + We restrict ourselves to the case where all symbols operate on a + single fixed type. In particular, this means that we cannot handle + situations like + + [H: forall x y, nat_of_pos (pos_of_nat (x) + y) + x = ....] + + where one occurrence of [+] operates on nat while the other one + operates on positive. *) + +Require Import Arith NArith. +Require Import List. +Require Import FMapPositive FMapFacts. +Require Import RelationClasses Equality. +Require Export Morphisms. + +From AAC_tactics +Require Import Utils. + +Set Implicit Arguments. +Set Asymmetric Patterns. + +Local Open Scope signature_scope. + +(** * Environments for the reification process: we use positive maps to index elements *) + +Section sigma. + Definition sigma := PositiveMap.t. + Definition sigma_get A (null : A) (map : sigma A) (n : positive) : A := + match PositiveMap.find n map with + | None => null + | Some x => x + end. + Definition sigma_add := @PositiveMap.add. + Definition sigma_empty := @PositiveMap.empty. +End sigma. + + +(** * Classes for properties of operators *) + +Class Associative (X:Type) (R:relation X) (dot: X -> X -> X) := + law_assoc : forall x y z, R (dot x (dot y z)) (dot (dot x y) z). +Class Commutative (X:Type) (R: relation X) (plus: X -> X -> X) := + law_comm: forall x y, R (plus x y) (plus y x). +Class Unit (X:Type) (R:relation X) (op : X -> X -> X) (unit:X) := { + law_neutral_left: forall x, R (op unit x) x; + law_neutral_right: forall x, R (op x unit) x +}. + + +(** Class used to find the equivalence relation on which operations + are A or AC, starting from the relation appearing in the goal *) + +Class AAC_lift X (R: relation X) (E : relation X) := { + aac_lift_equivalence : Equivalence E; + aac_list_proper : Proper (E ==> E ==> iff) R +}. + +(** simple instances, when we have a subrelation, or an equivalence *) + +Instance aac_lift_subrelation {X} {R} {E} {HE: Equivalence E} + {HR: @Transitive X R} {HER: subrelation E R}: AAC_lift R E | 3. +Proof. + constructor; trivial. + intros ? ? H ? ? H'. split; intro G. + rewrite <- H, G. apply HER, H'. + rewrite H, G. apply HER. symmetry. apply H'. +Qed. + +Instance aac_lift_proper {X} {R : relation X} {E} {HE: Equivalence E} + {HR: Proper (E==>E==>iff) R}: AAC_lift R E | 4 := {}. + + + +Module Internal. +(** * Utilities for the evaluation function *) + +Section copy. + + Context {X} {R} {HR: @Equivalence X R} {plus} + (op: Associative R plus) (op': Commutative R plus) (po: Proper (R ==> R ==> R) plus). + + (* copy n x = x+...+x (n times) *) + Fixpoint copy' n x := match n with + | xH => x + | xI n => let xn := copy' n x in plus (plus xn xn) x + | xO n => let xn := copy' n x in (plus xn xn) + end. + Definition copy n x := Prect (fun _ => X) x (fun _ xn => plus x xn) n. + + Lemma copy_plus : forall n m x, R (copy (n+m) x) (plus (copy n x) (copy m x)). + Proof. + unfold copy. + induction n using Pind; intros m x. + rewrite Prect_base. rewrite <- Pplus_one_succ_l. rewrite Prect_succ. reflexivity. + rewrite Pplus_succ_permute_l. rewrite 2Prect_succ. rewrite IHn. apply op. + Qed. + Lemma copy_xH : forall x, R (copy 1 x) x. + Proof. intros; unfold copy; rewrite Prect_base. reflexivity. Qed. + Lemma copy_Psucc : forall n x, R (copy (Pos.succ n) x) (plus x (copy n x)). + Proof. intros; unfold copy; rewrite Prect_succ. reflexivity. Qed. + + Global Instance copy_compat n: Proper (R ==> R) (copy n). + Proof. + unfold copy. + induction n using Pind; intros x y H. + rewrite 2Prect_base. assumption. + rewrite 2Prect_succ. apply po; auto. + Qed. + +End copy. + +(** * Packaging structures *) + +(** ** free symbols *) + +Module Sym. + Section t. + Context {X} {R : relation X} . + + (** type of an arity *) + Fixpoint type_of (n: nat) := + match n with + | O => X + | S n => X -> type_of n + end. + + (** relation to be preserved at an arity *) + Fixpoint rel_of n : relation (type_of n) := + match n with + | O => R + | S n => respectful R (rel_of n) + end. + + (** a symbol package contains an arity, + a value of the corresponding type, + and a proof that the value is a proper morphism *) + Record pack : Type := mkPack { + ar : nat; + value :> type_of ar; + morph : Proper (rel_of ar) value + }. + + (** helper to build default values, when filling reification environments *) + Definition null: pack := mkPack 1 (fun x => x) (fun _ _ H => H). + + End t. + +End Sym. + +(** ** binary operations *) + +Module Bin. + Section t. + Context {X} {R: relation X}. + + Record pack := mk_pack { + value:> X -> X -> X; + compat: Proper (R ==> R ==> R) value; + assoc: Associative R value; + comm: option (Commutative R value) + }. + End t. + (* See #Instances.v# for concrete instances of these classes. *) + +End Bin. + + +(** * Reification, normalisation, and decision *) + +Section s. + Context {X} {R: relation X} {E: @Equivalence X R}. + Infix "==" := R (at level 80). + + (* We use environments to store the various operators and the + morphisms.*) + + Variable e_sym: idx -> @Sym.pack X R. + Variable e_bin: idx -> @Bin.pack X R. + + + (** packaging units (depends on e_bin) *) + + Record unit_of u := mk_unit_for { + uf_idx: idx; + uf_desc: Unit R (Bin.value (e_bin uf_idx)) u + }. + + Record unit_pack := mk_unit_pack { + u_value:> X; + u_desc: list (unit_of u_value) + }. + Variable e_unit: positive -> unit_pack. + + Hint Resolve e_bin e_unit: typeclass_instances. + + (** ** Almost normalised syntax + a term in [T] is in normal form if: + - sums do not contain sums + - products do not contain products + - there are no unary sums or products + - lists and msets are lexicographically sorted according to the order we define below + + [vT n] denotes the set of term vectors of size [n] (the mutual dependency could be removed), + + Note that [T] and [vT] depend on the [e_sym] environment (which + contains, among other things, the arity of symbols) + *) + + Inductive T: Type := + | sum: idx -> mset T -> T + | prd: idx -> nelist T -> T + | sym: forall i, vT (Sym.ar (e_sym i)) -> T + | unit : idx -> T + with vT: nat -> Type := + | vnil: vT O + | vcons: forall n, T -> vT n -> vT (S n). + + + (** lexicographic rpo over the normalised syntax *) + Fixpoint compare (u v: T) := + match u,v with + | sum i l, sum j vs => lex (idx_compare i j) (mset_compare compare l vs) + | prd i l, prd j vs => lex (idx_compare i j) (list_compare compare l vs) + | sym i l, sym j vs => lex (idx_compare i j) (vcompare l vs) + | unit i , unit j => idx_compare i j + | unit _ , _ => Lt + | _ , unit _ => Gt + | sum _ _, _ => Lt + | _ , sum _ _ => Gt + | prd _ _, _ => Lt + | _ , prd _ _ => Gt + + end + with vcompare i j (us: vT i) (vs: vT j) := + match us,vs with + | vnil, vnil => Eq + | vnil, _ => Lt + | _, vnil => Gt + | vcons _ u us, vcons _ v vs => lex (compare u v) (vcompare us vs) + end. + + + + (** ** Evaluation from syntax to the abstract domain *) + + Fixpoint eval u: X := + match u with + | sum i l => let o := Bin.value (e_bin i) in + fold_map (fun un => let '(u,n):=un in @copy _ o n (eval u)) o l + | prd i l => fold_map eval (Bin.value (e_bin i)) l + | sym i v => eval_aux v (Sym.value (e_sym i)) + | unit i => e_unit i + end + with eval_aux i (v: vT i): Sym.type_of i -> X := + match v with + | vnil => fun f => f + | vcons _ u v => fun f => eval_aux v (f (eval u)) + end. + + (** we need to show that compare reflects equality (this is because + we work with msets rather than lists with arities) *) + Lemma tcompare_weak_spec: forall (u v : T), compare_weak_spec u v (compare u v) + with vcompare_reflect_eqdep: forall i us j vs (H: i=j), vcompare us vs = Eq -> cast vT H us = vs. + Proof. + induction u. + destruct v; simpl; try constructor. + case (pos_compare_weak_spec p p0); intros; try constructor. + case (mset_compare_weak_spec compare tcompare_weak_spec m m0); intros; try constructor. + destruct v; simpl; try constructor. + case (pos_compare_weak_spec p p0); intros; try constructor. + case (list_compare_weak_spec compare tcompare_weak_spec n n0); intros; try constructor. + destruct v0; simpl; try constructor. + case_eq (idx_compare i i0); intro Hi; try constructor. + apply idx_compare_reflect_eq in Hi. symmetry in Hi. subst. (* the [symmetry] is required ! *) + case_eq (vcompare v v0); intro Hv; try constructor. + rewrite <- (vcompare_reflect_eqdep _ _ _ _ eq_refl Hv). constructor. + destruct v; simpl; try constructor. + case_eq (idx_compare p p0); intro Hi; try constructor. + apply idx_compare_reflect_eq in Hi. symmetry in Hi. subst. constructor. + + induction us; destruct vs; simpl; intros H Huv; try discriminate. + apply cast_eq, eq_nat_dec. + injection H; intro Hn. + revert Huv; case (tcompare_weak_spec t t0); intros; try discriminate. + symmetry in Hn. subst. (* symmetry required *) + rewrite <- (IHus _ _ eq_refl Huv). + apply cast_eq, eq_nat_dec. + Qed. + + Instance eval_aux_compat i (l: vT i): Proper (@Sym.rel_of X R i ==> R) (eval_aux l). + Proof. + induction l; simpl; repeat intro. + assumption. + apply IHl, H. reflexivity. + Qed. + + + (* is [i] a unit for [j] ? *) + Definition is_unit_of j i := + List.existsb (fun p => eq_idx_bool j (uf_idx p)) (u_desc (e_unit i)). + + (* is [i] commutative ? *) + Definition is_commutative i := + match Bin.comm (e_bin i) with Some _ => true | None => false end. + + + (** ** Normalisation *) + + Inductive discr {A} : Type := + | Is_op : A -> discr + | Is_unit : idx -> discr + | Is_nothing : discr . + + (* This is called sum in the std lib *) + Inductive m {A} {B} := + | left : A -> m + | right : B -> m. + + Definition comp A B (merge : B -> B -> B) (l : B) (l' : @m A B) : @m A B := + match l' with + | left _ => right l + | right l' => right (merge l l') + end. + + (** auxiliary functions, to clean up sums *) + + Section sums. + Variable i : idx. + Variable is_unit : idx -> bool. + + Definition sum' (u: mset T): T := + match u with + | nil (u,xH) => u + | _ => sum i u + end. + + Definition is_sum (u: T) : @discr (mset T) := + match u with + | sum j l => if eq_idx_bool j i then Is_op l else Is_nothing + | unit j => if is_unit j then Is_unit j else Is_nothing + | u => Is_nothing + end. + + Definition copy_mset n (l: mset T): mset T := + match n with + | xH => l + | _ => nelist_map (fun vm => let '(v,m):=vm in (v,Pmult n m)) l + end. + + Definition return_sum u n := + match is_sum u with + | Is_nothing => right (nil (u,n)) + | Is_op l' => right (copy_mset n l') + | Is_unit j => left j + end. + + Definition add_to_sum u n (l : @m idx (mset T)) := + match is_sum u with + | Is_nothing => comp (merge_msets compare) (nil (u,n)) l + | Is_op l' => comp (merge_msets compare) (copy_mset n l') l + | Is_unit _ => l + end. + + + Definition norm_msets_ norm (l: mset T) := + fold_map' + (fun un => let '(u,n) := un in return_sum (norm u) n) + (fun un l => let '(u,n) := un in add_to_sum (norm u) n l) l. + + + End sums. + + (** similar functions for products *) + + Section prds. + + Variable i : idx. + Variable is_unit : idx -> bool. + Definition prd' (u: nelist T): T := + match u with + | nil u => u + | _ => prd i u + end. + + Definition is_prd (u: T) : @discr (nelist T) := + match u with + | prd j l => if eq_idx_bool j i then Is_op l else Is_nothing + | unit j => if is_unit j then Is_unit j else Is_nothing + | u => Is_nothing + end. + + + Definition return_prd u := + match is_prd u with + | Is_nothing => right (nil (u)) + | Is_op l' => right (l') + | Is_unit j => left j + end. + + Definition add_to_prd u (l : @m idx (nelist T)) := + match is_prd u with + | Is_nothing => comp (@appne T) (nil (u)) l + | Is_op l' => comp (@appne T) (l') l + | Is_unit _ => l + end. + + Definition norm_lists_ norm (l : nelist T) := + fold_map' + (fun u => return_prd (norm u)) + (fun u l => add_to_prd (norm u) l) l. + + + End prds. + + + Definition run_list x := match x with + | left n => nil (unit n) + | right l => l + end. + + Definition norm_lists norm i l := + let is_unit := is_unit_of i in + run_list (norm_lists_ i is_unit norm l). + + Definition run_msets x := match x with + | left n => nil (unit n, xH) + | right l => l + end. + + Definition norm_msets norm i l := + let is_unit := is_unit_of i in + run_msets (norm_msets_ i is_unit norm l). + + Fixpoint norm u {struct u}:= + match u with + | sum i l => if is_commutative i then sum' i (norm_msets norm i l) else u + | prd i l => prd' i (norm_lists norm i l) + | sym i l => sym i (vnorm l) + | unit i => unit i + end + with vnorm i (l: vT i): vT i := + match l with + | vnil => vnil + | vcons _ u l => vcons (norm u) (vnorm l) + end. + + (** ** Correctness *) + + Lemma is_unit_of_Unit : forall i j : idx, + is_unit_of i j = true -> Unit R (Bin.value (e_bin i)) (eval (unit j)). + Proof. + intros. unfold is_unit_of in H. + rewrite existsb_exists in H. + destruct H as [x [H H']]. + revert H' ; case (eq_idx_spec); [intros H' _ ; subst| intros _ H'; discriminate]. + simpl. destruct x. simpl. auto. + Qed. + + Instance Binvalue_Commutative i (H : is_commutative i = true) : Commutative R (@Bin.value _ _ (e_bin i) ). + Proof. + unfold is_commutative in H. + destruct (Bin.comm (e_bin i)); auto. + discriminate. + Qed. + + Instance Binvalue_Associative i :Associative R (@Bin.value _ _ (e_bin i) ). + Proof. + destruct ((e_bin i)); auto. + Qed. + + Instance Binvalue_Proper i : Proper (R ==> R ==> R) (@Bin.value _ _ (e_bin i) ). + Proof. + destruct ((e_bin i)); auto. + Qed. + Hint Resolve Binvalue_Proper Binvalue_Associative Binvalue_Commutative. + + (** auxiliary lemmas about sums *) + + Hint Resolve is_unit_of_Unit. + Section sum_correctness. + Variable i : idx. + Variable is_unit : idx -> bool. + Hypothesis is_unit_sum_Unit : forall j, is_unit j = true-> @Unit X R (Bin.value (e_bin i)) (eval (unit j)). + + Inductive is_sum_spec_ind : T -> @discr (mset T) -> Prop := + | is_sum_spec_op : forall j l, j = i -> is_sum_spec_ind (sum j l) (Is_op l) + | is_sum_spec_unit : forall j, is_unit j = true -> is_sum_spec_ind (unit j) (Is_unit j) + | is_sum_spec_nothing : forall u, is_sum_spec_ind u (Is_nothing). + + Lemma is_sum_spec u : is_sum_spec_ind u (is_sum i is_unit u). + Proof. + unfold is_sum; case u; intros; try constructor. + case_eq (eq_idx_bool p i); intros; subst; try constructor; auto. + revert H. case eq_idx_spec; try discriminate. auto. + case_eq (is_unit p); intros; try constructor. auto. + Qed. + + Instance assoc : @Associative X R (Bin.value (e_bin i)). + Proof. + destruct (e_bin i). simpl. assumption. + Qed. + Instance proper : Proper (R ==> R ==> R)(Bin.value (e_bin i)). + Proof. + destruct (e_bin i). simpl. assumption. + Qed. + Hypothesis comm : @Commutative X R (Bin.value (e_bin i)). + + Lemma sum'_sum : forall (l: mset T), eval (sum' i l) ==eval (sum i l) . + Proof. + intros [[a n] | [a n] l]; destruct n; simpl; reflexivity. + Qed. + + Lemma eval_sum_nil x: + eval (sum i (nil (x,xH))) == (eval x). + Proof. rewrite <- sum'_sum. reflexivity. Qed. + + Lemma eval_sum_cons : forall n a (l: mset T), + (eval (sum i ((a,n)::l))) == (@Bin.value _ _ (e_bin i) (@copy _ (@Bin.value _ _ (e_bin i)) n (eval a)) (eval (sum i l))). + Proof. + intros n a [[? ? ]|[b m] l]; simpl; reflexivity. + Qed. + + Inductive compat_sum_unit : @m idx (mset T) -> Prop := + | csu_left : forall x, is_unit x = true-> compat_sum_unit (left x) + | csu_right : forall m, compat_sum_unit (right m) + . + + Lemma compat_sum_unit_return x n : compat_sum_unit (return_sum i is_unit x n). + Proof. + unfold return_sum. + case is_sum_spec; intros; try constructor; auto. + Qed. + + Lemma compat_sum_unit_add : forall x n h, + compat_sum_unit h + -> + compat_sum_unit + (add_to_sum i (is_unit_of i) x n + h). + Proof. + unfold add_to_sum;intros; inversion H; + case_eq (is_sum i (is_unit_of i) x); + intros; simpl; try constructor || eauto. apply H0. + Qed. + + (* Hint Resolve copy_plus. : this lags because of the inference of the implicit arguments *) + Hint Extern 5 (copy (?n + ?m) (eval ?a) == Bin.value (copy ?n (eval ?a)) (copy ?m (eval ?a))) => apply copy_plus. + Hint Extern 5 (?x == ?x) => reflexivity. + Hint Extern 5 ( Bin.value ?x ?y == Bin.value ?y ?x) => apply Bin.comm. + + Lemma eval_merge_bin : forall (h k: mset T), + eval (sum i (merge_msets compare h k)) == @Bin.value _ _ (e_bin i) (eval (sum i h)) (eval (sum i k)). + Proof. + induction h as [[a n]|[a n] h IHh]; intro k. + simpl. + induction k as [[b m]|[b m] k IHk]; simpl. + destruct (tcompare_weak_spec a b) as [a|a b|a b]; simpl; auto. apply copy_plus; auto. + + destruct (tcompare_weak_spec a b) as [a|a b|a b]; simpl; auto. + rewrite copy_plus,law_assoc; auto. + rewrite IHk; clear IHk. rewrite 2 law_assoc. apply proper. apply law_comm. reflexivity. + + induction k as [[b m]|[b m] k IHk]; simpl; simpl in IHh. + destruct (tcompare_weak_spec a b) as [a|a b|a b]; simpl. + rewrite (law_comm _ (copy m (eval a))), law_assoc, <- copy_plus, Pplus_comm; auto. + rewrite <- law_assoc, IHh. reflexivity. + rewrite law_comm. reflexivity. + + simpl in IHk. + destruct (tcompare_weak_spec a b) as [a|a b|a b]; simpl. + rewrite IHh; clear IHh. rewrite 2 law_assoc. rewrite (law_comm _ (copy m (eval a))). rewrite law_assoc, <- copy_plus, Pplus_comm; auto. + rewrite IHh; clear IHh. simpl. rewrite law_assoc. reflexivity. + rewrite 2 (law_comm (copy m (eval b))). rewrite law_assoc. apply proper; [ | reflexivity]. + rewrite <- IHk. reflexivity. + Qed. + + + Lemma copy_mset' n (l: mset T): copy_mset n l = nelist_map (fun vm => let '(v,m):=vm in (v,Pmult n m)) l. + Proof. + unfold copy_mset. destruct n; try reflexivity. + + simpl. induction l as [|[a l] IHl]; simpl; try congruence. destruct a. reflexivity. + Qed. + + + Lemma copy_mset_succ n (l: mset T): eval (sum i (copy_mset (Pos.succ n) l)) == @Bin.value _ _ (e_bin i) (eval (sum i l)) (eval (sum i (copy_mset n l))). + Proof. + rewrite 2 copy_mset'. + + induction l as [[a m]|[a m] l IHl]. + simpl eval. rewrite <- copy_plus; auto. rewrite Pmult_Sn_m. reflexivity. + + simpl nelist_map. rewrite ! eval_sum_cons. rewrite IHl. clear IHl. + rewrite Pmult_Sn_m. rewrite copy_plus; auto. rewrite <- !law_assoc. + apply Binvalue_Proper; try reflexivity. + rewrite law_comm . rewrite <- !law_assoc. apply proper; try reflexivity. + apply law_comm. + Qed. + + Lemma copy_mset_copy : forall n (m : mset T), eval (sum i (copy_mset n m)) == @copy _ (@Bin.value _ _ (e_bin i)) n (eval (sum i m)). + Proof. + induction n using Pind; intros. + + unfold copy_mset. rewrite copy_xH. reflexivity. + rewrite copy_mset_succ. rewrite copy_Psucc. rewrite IHn. reflexivity. + Qed. + + Instance compat_sum_unit_Unit : forall p, compat_sum_unit (left p) -> + @Unit X R (Bin.value (e_bin i)) (eval (unit p)). + Proof. + intros. + inversion H. subst. auto. + Qed. + + Lemma copy_n_unit : forall j n, is_unit j = true -> + eval (unit j) == @copy _ (Bin.value (e_bin i)) n (eval (unit j)). + Proof. + intros. + induction n using Prect. + rewrite copy_xH. reflexivity. + rewrite copy_Psucc. rewrite <- IHn. apply is_unit_sum_Unit in H. rewrite law_neutral_left. reflexivity. + Qed. + + + Lemma z0 l r (H : compat_sum_unit r): + eval (sum i (run_msets (comp (merge_msets compare) l r))) == eval (sum i ((merge_msets compare) (l) (run_msets r))). + Proof. + unfold comp. unfold run_msets. + case_eq r; intros; subst. + rewrite eval_merge_bin; auto. + rewrite eval_sum_nil. + apply compat_sum_unit_Unit in H. rewrite law_neutral_right. reflexivity. + reflexivity. + Qed. + + Lemma z1 : forall n x, + eval (sum i (run_msets (return_sum i (is_unit) x n ))) + == @copy _ (@Bin.value _ _ (e_bin i)) n (eval x). + Proof. + intros. unfold return_sum. unfold run_msets. + case (is_sum_spec); intros; subst. + rewrite copy_mset_copy. + reflexivity. + + rewrite eval_sum_nil. apply copy_n_unit. auto. + reflexivity. + Qed. + Lemma z2 : forall u n x, compat_sum_unit x -> + eval (sum i ( run_msets + (add_to_sum i (is_unit) u n x))) + == + @Bin.value _ _ (e_bin i) (@copy _ (@Bin.value _ _ (e_bin i)) n (eval u)) (eval (sum i (run_msets x))). + Proof. + intros u n x Hix . + unfold add_to_sum. + case is_sum_spec; intros; subst. + + rewrite z0 by auto. rewrite eval_merge_bin. rewrite copy_mset_copy. reflexivity. + rewrite <- copy_n_unit by assumption. + apply is_unit_sum_Unit in H. + rewrite law_neutral_left. reflexivity. + + + rewrite z0 by auto. rewrite eval_merge_bin. reflexivity. + Qed. + End sum_correctness. + Lemma eval_norm_msets i norm + (Comm : Commutative R (Bin.value (e_bin i))) + (Hnorm: forall u, eval (norm u) == eval u) : forall h, eval (sum i (norm_msets norm i h)) == eval (sum i h). + Proof. + unfold norm_msets. + assert (H : + forall h : mset T, + eval (sum i (run_msets (norm_msets_ i (is_unit_of i) norm h))) == eval (sum i h) /\ compat_sum_unit (is_unit_of i) (norm_msets_ i (is_unit_of i) norm h)). + + induction h as [[a n] | [a n] h [IHh IHh']]; simpl norm_msets_; split. + rewrite z1 by auto. rewrite Hnorm . reflexivity. auto. + apply compat_sum_unit_return. + + rewrite z2 by auto. rewrite IHh. + rewrite eval_sum_cons. rewrite Hnorm. reflexivity. apply compat_sum_unit_add, IHh'. + + apply H. + Defined. + + (** auxiliary lemmas about products *) + + Section prd_correctness. + Variable i : idx. + Variable is_unit : idx -> bool. + Hypothesis is_unit_prd_Unit : forall j, is_unit j = true-> @Unit X R (Bin.value (e_bin i)) (eval (unit j)). + + Inductive is_prd_spec_ind : T -> @discr (nelist T) -> Prop := + | is_prd_spec_op : + forall j l, j = i -> is_prd_spec_ind (prd j l) (Is_op l) + | is_prd_spec_unit : + forall j, is_unit j = true -> is_prd_spec_ind (unit j) (Is_unit j) + | is_prd_spec_nothing : + forall u, is_prd_spec_ind u (Is_nothing). + + Lemma is_prd_spec u : is_prd_spec_ind u (is_prd i is_unit u). + Proof. + unfold is_prd; case u; intros; try constructor. + case (eq_idx_spec); intros; subst; try constructor; auto. + case_eq (is_unit p); intros; try constructor; auto. + Qed. + + Lemma prd'_prd : forall (l: nelist T), eval (prd' i l) == eval (prd i l). + Proof. + intros [?|? [|? ?]]; simpl; reflexivity. + Qed. + + + Lemma eval_prd_nil x: eval (prd i (nil x)) == eval x. + Proof. + rewrite <- prd'_prd. simpl. reflexivity. + Qed. + Lemma eval_prd_cons a : forall (l: nelist T), eval (prd i (a::l)) == @Bin.value _ _ (e_bin i) (eval a) (eval (prd i l)). + Proof. + intros [|b l]; simpl; reflexivity. + Qed. + Lemma eval_prd_app : forall (h k: nelist T), eval (prd i (h++k)) == @Bin.value _ _ (e_bin i) (eval (prd i h)) (eval (prd i k)). + Proof. + induction h; intro k. simpl; try reflexivity. + simpl appne. rewrite 2 eval_prd_cons, IHh, law_assoc. reflexivity. + Qed. + + Inductive compat_prd_unit : @m idx (nelist T) -> Prop := + | cpu_left : forall x, is_unit x = true -> compat_prd_unit (left x) + | cpu_right : forall m, compat_prd_unit (right m) + . + + Lemma compat_prd_unit_return x: compat_prd_unit (return_prd i is_unit x). + Proof. + unfold return_prd. + case (is_prd_spec); intros; try constructor; auto. + Qed. + + Lemma compat_prd_unit_add : forall x h, + compat_prd_unit h + -> + compat_prd_unit + (add_to_prd i is_unit x + h). + Proof. + intros. + unfold add_to_prd. + unfold comp. + case (is_prd_spec); intros; try constructor; auto. + unfold comp; case h; try constructor. + unfold comp; case h; try constructor. + Qed. + + + Instance compat_prd_Unit : forall p, compat_prd_unit (left p) -> + @Unit X R (Bin.value (e_bin i)) (eval (unit p)). + Proof. + intros. + inversion H; subst. apply is_unit_prd_Unit. assumption. + Qed. + + Lemma z0' : forall l (r: @m idx (nelist T)), compat_prd_unit r -> + eval (prd i (run_list (comp (@appne T) l r))) == eval (prd i ((appne (l) (run_list r)))). + Proof. + intros. + unfold comp. unfold run_list. case_eq r; intros; auto; subst. + rewrite eval_prd_app. + rewrite eval_prd_nil. + apply compat_prd_Unit in H. rewrite law_neutral_right. reflexivity. + reflexivity. + Qed. + + Lemma z1' a : eval (prd i (run_list (return_prd i is_unit a))) == eval (prd i (nil a)). + Proof. + intros. unfold return_prd. unfold run_list. + case (is_prd_spec); intros; subst; reflexivity. + Qed. + Lemma z2' : forall u x, compat_prd_unit x -> + eval (prd i ( run_list + (add_to_prd i is_unit u x))) == @Bin.value _ _ (e_bin i) (eval u) (eval (prd i (run_list x))). + Proof. + intros u x Hix. + unfold add_to_prd. + case (is_prd_spec); intros; subst. + rewrite z0' by auto. rewrite eval_prd_app. reflexivity. + apply is_unit_prd_Unit in H. rewrite law_neutral_left. reflexivity. + rewrite z0' by auto. rewrite eval_prd_app. reflexivity. + Qed. + + End prd_correctness. + + + + + Lemma eval_norm_lists i (Hnorm: forall u, eval (norm u) == eval u) : forall h, eval (prd i (norm_lists norm i h)) == eval (prd i h). + Proof. + unfold norm_lists. + assert (H : forall h : nelist T, + eval (prd i (run_list (norm_lists_ i (is_unit_of i) norm h))) == + eval (prd i h) + /\ compat_prd_unit (is_unit_of i) (norm_lists_ i (is_unit_of i) norm h)). + + + induction h as [a | a h [IHh IHh']]; simpl norm_lists_; split. + rewrite z1'. simpl. apply Hnorm. + + apply compat_prd_unit_return. + + rewrite z2'. rewrite IHh. rewrite eval_prd_cons. rewrite Hnorm. reflexivity. apply is_unit_of_Unit. + auto. + + apply compat_prd_unit_add. auto. + apply H. + Defined. + + (** correctness of the normalisation function *) + + Theorem eval_norm: forall u, eval (norm u) == eval u + with eval_norm_aux: forall i (l: vT i) (f: Sym.type_of i), + Proper (@Sym.rel_of X R i) f -> eval_aux (vnorm l) f == eval_aux l f. + Proof. + induction u as [ p m | p l | ? | ?]; simpl norm. + case_eq (is_commutative p); intros. + rewrite sum'_sum. + apply eval_norm_msets; auto. + reflexivity. + + rewrite prd'_prd. + apply eval_norm_lists; auto. + + apply eval_norm_aux, Sym.morph. + + reflexivity. + + induction l; simpl; intros f Hf. reflexivity. + rewrite eval_norm. apply IHl, Hf; reflexivity. + Qed. + + + (** corollaries, for goal normalisation or decision *) + + Lemma normalise : forall (u v: T), eval (norm u) == eval (norm v) -> eval u == eval v. + Proof. intros u v. rewrite 2 eval_norm. trivial. Qed. + + Lemma compare_reflect_eq: forall u v, compare u v = Eq -> eval u == eval v. + Proof. intros u v. case (tcompare_weak_spec u v); intros; try congruence. reflexivity. Qed. + + Lemma decide: forall (u v: T), compare (norm u) (norm v) = Eq -> eval u == eval v. + Proof. intros u v H. apply normalise. apply compare_reflect_eq. apply H. Qed. + + Lemma lift_normalise {S} {H : AAC_lift S R}: + forall (u v: T), (let x := norm u in let y := norm v in + S (eval x) (eval y)) -> S (eval u) (eval v). + Proof. destruct H. intros u v; simpl; rewrite 2 eval_norm. trivial. Qed. + +End s. +End Internal. + +Local Ltac internal_normalize := + let x := fresh in let y := fresh in + intro x; intro y; vm_compute in x; vm_compute in y; unfold x; unfold y; + compute [Internal.eval Utils.fold_map Internal.copy Prect]; simpl. + + +(** * Lemmas for performing transitivity steps + given an instance of AAC_lift *) + +Section t. + Context `{AAC_lift}. + + Lemma lift_transitivity_left (y x z : X): E x y -> R y z -> R x z. + Proof. destruct H as [Hequiv Hproper]; intros G;rewrite G. trivial. Qed. + + Lemma lift_transitivity_right (y x z : X): E y z -> R x y -> R x z. + Proof. destruct H as [Hequiv Hproper]; intros G. rewrite G. trivial. Qed. + + Lemma lift_reflexivity {HR :Reflexive R}: forall x y, E x y -> R x y. + Proof. destruct H. intros ? ? G. rewrite G. reflexivity. Qed. + +End t. + +Declare ML Module "aac_plugin". diff --git a/theories/Caveats.v b/theories/Caveats.v new file mode 100644 index 0000000..d7824cd --- /dev/null +++ b/theories/Caveats.v @@ -0,0 +1,376 @@ +(***************************************************************************) +(* This is part of aac_tactics, it is distributed under the terms of the *) +(* GNU Lesser General Public License version 3 *) +(* (see file LICENSE for more details) *) +(* *) +(* Copyright 2009-2010: Thomas Braibant, Damien Pous. *) +(***************************************************************************) + +(** * Currently known caveats and limitations of the [aac_tactics] library. + + Depending on your installation, either uncomment the following two + lines, or add them to your .coqrc files, replacing "." + with the path to the [aac_tactics] library +*) + +Require NArith Minus. + +From AAC_tactics +Require Import AAC. +From AAC_tactics +Require Instances. + +(** ** Limitations *) + +(** *** 1. Dependent parameters + The type of the rewriting hypothesis must be of the form + + [forall (x_1: T_1) ... (x_n: T_n), R l r], + + where [R] is a relation over some type [T] and such that for all + variable [x_i] appearing in the left-hand side ([l]), we actually + have [T_i]=[T]. The goal should be of the form [S g d], where [S] + is a relation on [T]. + + In other words, we cannot instantiate arguments of an exogeneous + type. *) + +Section parameters. + + Context {X} {R} {E: @Equivalence X R} + {plus} {plus_A: Associative R plus} {plus_C: Commutative R plus} + {plus_Proper: Proper (R ==> R ==> R) plus} + {zero} {Zero: Unit R plus zero}. + + Notation "x == y" := (R x y) (at level 70). + Notation "x + y" := (plus x y) (at level 50, left associativity). + Notation "0" := (zero). + + Variable f: nat -> X -> X. + + (** in [Hf], the parameter [n] has type [nat], it cannot be instantiated automatically *) + Hypothesis Hf: forall n x, f n x + x == x. + Hypothesis Hf': forall n, Proper (R ==> R) (f n). + + Goal forall a b k, a + f k (b+a) + b == a+b. + intros. + Fail aac_rewrite Hf. (** [aac_rewrite] does not instantiate [n] automatically *) + aac_rewrite (Hf k). (** of course, this argument can be given explicitly *) + aac_reflexivity. + Qed. + + (** for the same reason, we cannot handle higher-order parameters (here, [g])*) + Hypothesis H : forall g x y, g x + g y == g (x + y). + Variable g : X -> X. + Hypothesis Hg : Proper (R ==> R) g. + Goal forall a b c, g a + g b + g c == g (a + b + c). + intros. + Fail aac_rewrite H. + do 2 aac_rewrite (H g). aac_reflexivity. + Qed. + +End parameters. + + +(** *** 2. Exogeneous morphisms + + We do not handle `exogeneous' morphisms: morphisms that move from + type [T] to some other type [T']. *) + +Section morphism. + Import NArith Minus. + Open Scope nat_scope. + + (** Typically, although [N_of_nat] is a proper morphism from + [@eq nat] to [@eq N], we cannot rewrite under [N_of_nat] *) + Goal forall a b: nat, N_of_nat (a+b-(b+a)) = 0%N. + intros. + Fail aac_rewrite minus_diag. + Abort. + + + (* More generally, this prevents us from rewriting under + propositional contexts *) + Context {P} {HP : Proper (@eq nat ==> iff) P}. + Hypothesis H : P 0. + + Goal forall a b, P (a + b - (b + a)). + intros a b. + Fail aac_rewrite minus_diag. + (** a solution is to introduce an evar to replace the part to be + rewritten. This tiresome process should be improved in the + future. Here, it can be done using eapply and the morphism. *) + eapply HP. + aac_rewrite minus_diag. + reflexivity. + exact H. + Qed. + + Goal forall a b, a+b-(b+a) = 0 /\ b-b = 0. + intros. + (** similarly, we need to bring equations to the toplevel before + being able to rewrite *) + Fail aac_rewrite minus_diag. + split; aac_rewrite minus_diag; reflexivity. + Qed. + +End morphism. + + +(** *** 3. Treatment of variance with inequations. + + We do not take variance into account when we compute the set of + solutions to a matching problem modulo AC. As a consequence, + [aac_instances] may propose solutions for which [aac_rewrite] will + fail, due to the lack of adequate morphisms *) + +Section ineq. + + Import ZArith. + Import Instances.Z. + Open Scope Z_scope. + + Instance Zplus_incr: Proper (Z.le ==> Z.le ==> Z.le) Zplus. + Proof. intros ? ? H ? ? H'. apply Zplus_le_compat; assumption. Qed. + + Hypothesis H: forall x, x+x <= x. + Goal forall a b c, c + - (a + a) + b + b <= c. + intros. + (** this fails because the first solution is not valid ([Zopp] is not increasing), *) + Fail aac_rewrite H. + aac_instances H. + (** on the contrary, the second solution is valid: *) + aac_rewrite H at 1. + (** Currently, we cannot filter out such invalid solutions in an easy way; + this should be fixed in the future *) + Abort. + +End ineq. + + + +(** ** Caveats *) + +(** *** 1. Special treatment for units. + [S O] is considered as a unit for multiplication whenever a [Peano.mult] + appears in the goal. The downside is that [S x] does not match [1], + and [1] does not match [S(0+0)] whenever [Peano.mult] appears in + the goal. *) + +Section Peano. + Import Instances.Peano. + + Hypothesis H : forall x, x + S x = S (x+x). + + Goal 1 = 1. + (** ok (no multiplication around), [x] is instantiated with [O] *) + aacu_rewrite H. + Abort. + + Goal 1*1 = 1. + (** fails since 1 is seen as a unit, not the application of the + morphism [S] to the constant [O] *) + Fail aacu_rewrite H. + Abort. + + Hypothesis H': forall x, x+1 = 1+x. + + Goal forall a, a+S(0+0) = 1+a. + (** ok (no multiplication around), [x] is instantiated with [a]*) + intro. aac_rewrite H'. + Abort. + + Goal forall a, a*a+S(0+0) = 1+a*a. + (** fails: although [S(0+0)] is understood as the application of + the morphism [S] to the constant [O], it is not recognised + as the unit [S O] of multiplication *) + intro. Fail aac_rewrite H'. + Abort. + + (** More generally, similar counter-intuitive behaviours can appear + when declaring an applied morphism as an unit. *) + +End Peano. + + + +(** *** 2. Existential variables. +We implemented an algorithm for _matching_ modulo AC, not for +_unifying_ modulo AC. As a consequence, existential variables +appearing in a goal are considered as constants, they will not be +instantiated. *) + +Section evars. + Import ZArith. + Import Instances.Z. + + Variable P: Prop. + Hypothesis H: forall x y, x+y+x = x -> P. + Hypothesis idem: forall x, x+x = x. + Goal P. + eapply H. + aac_rewrite idem. (** this works: [x] is instantiated with an evar *) + instantiate (2 := 0). + symmetry. aac_reflexivity. (** this does work but there are remaining evars in the end *) + Abort. + + Hypothesis H': forall x, 3+x = x -> P. + Goal P. + eapply H'. + Fail aac_rewrite idem. (** this fails since we do not instantiate evars *) + Abort. +End evars. + + +(** *** 3. Distinction between [aac_rewrite] and [aacu_rewrite] *) + +Section U. + Context {X} {R} {E: @Equivalence X R} + {dot} {dot_A: Associative R dot} {dot_Proper: Proper (R ==> R ==> R) dot} + {one} {One: Unit R dot one}. + + Infix "==" := R (at level 70). + Infix "*" := dot. + Notation "1" := one. + + (** In some situations, the [aac_rewrite] tactic allows + instantiations of a variable with a unit, when the variable occurs + directly under a function symbol: *) + + Variable f : X -> X. + Hypothesis Hf : Proper (R ==> R) f. + Hypothesis dot_inv_left : forall x, f x*x == x. + Goal f 1 == 1. + aac_rewrite dot_inv_left. reflexivity. + Qed. + + (** This behaviour seems desirable in most situations: these + solutions with units are less peculiar than the other ones, since + the unit comes from the goal. However, this policy is not properly + enforced for now (hard to do with the current algorithm): *) + + Hypothesis dot_inv_right : forall x, x*f x == x. + Goal f 1 == 1. + Fail aac_rewrite dot_inv_right. + aacu_rewrite dot_inv_right. reflexivity. + Qed. + +End U. + +(** *** 4. Rewriting units *) +Section V. + Context {X} {R} {E: @Equivalence X R} + {dot} {dot_A: Associative R dot} {dot_Proper: Proper (R ==> R ==> R) dot} + {one} {One: Unit R dot one}. + + Infix "==" := R (at level 70). + Infix "*" := dot. + Notation "1" := one. + + (** [aac_rewrite] uses the symbols appearing in the goal and the + hypothesis to infer the AC and A operations. In the following + example, [dot] appears neither in the left-hand-side of the goal, + nor in the right-hand side of the hypothesis. Hence, 1 is not + recognised as a unit. To circumvent this problem, we can force + [aac_rewrite] to take into account a given operation, by giving + it an extra argument. This extra argument seems useful only in + this peculiar case. *) + + Lemma inv_unique: forall x y y', x*y == 1 -> y'*x == 1 -> y==y'. + Proof. + intros x y y' Hxy Hy'x. + aac_instances <- Hy'x [dot]. + aac_rewrite <- Hy'x at 1 [dot]. + aac_rewrite Hxy. aac_reflexivity. + Qed. +End V. + +(** *** 5. Rewriting too much things. *) +Section W. + Variables a b c: nat. + Hypothesis H: 0 = c. + + Goal b*(a+a) <= b*(c+a+a+1). + + (** [aac_rewrite] finds a pattern modulo AC that matches a given + hypothesis, and then makes a call to [setoid_rewrite]. This + [setoid_rewrite] can unfortunately make several rewrites (in a + non-intuitive way: below, the [1] in the right-hand side is + rewritten into [S c]) *) + aac_rewrite H. + + (** To this end, we provide a companion tactic to [aac_rewrite] + and [aacu_rewrite], that makes the transitivity step, but not the + setoid_rewrite: + + This allows the user to select the relevant occurrences in which + to rewrite. *) + aac_pattern H at 2. setoid_rewrite H at 1. + Abort. + +End W. + +(** *** 6. Rewriting nullifiable patterns. *) +Section Z. + +(** If the pattern of the rewritten hypothesis does not contain "hard" +symbols (like constants, function symbols, AC or A symbols without +units), there can be infinitely many subterms such that the pattern +matches: it is possible to build "subterms" modulo ACU that make the +size of the term increase (by making neutral elements appear in a +layered fashion). Hence, we settled with heuristics to propose only +"some" of these solutions. In such cases, the tactic displays a +(conservative) warning. *) + +Variables a b c: nat. +Variable f: nat -> nat. +Hypothesis H0: forall x, 0 = x - x. +Hypothesis H1: forall x, 1 = x * x. + +Goal a+b*c = c. + aac_instances H0. + (** In this case, only three solutions are proposed, while there are + infinitely many solutions. E.g. + - a+b*c*(1+[]) + - a+b*c*(1+0*(1+ [])) + - ... + *) +Abort. + +(** **** If the pattern is a unit or can be instantiated to be equal + to a unit: + + The heuristic is to make the unit appear at each possible position + in the term, e.g. transforming [a] into [1*a] and [a*1], but this + process is not recursive (we will not transform [1*a]) into + [(1+0*1)*a] *) + +Goal a+b+c = c. + + aac_instances H0 [mult]. + (** 1 solution, we miss solutions like [(a+b+c*(1+0*(1+[])))] and so on *) + + aac_instances H1 [mult]. + (** 7 solutions, we miss solutions like [(a+b+c+0*(1+0*[]))]*) +Abort. + +(** *** Another example of the former case is the following, where the hypothesis can be instantiated to be equal to [1] *) +Hypothesis H : forall x y, (x+y)*x = x*x + y *x. +Goal a*a+b*a + c = c. + (** Here, only one solution if we use the aac_instance tactic *) + aac_instances <- H. + + (** There are 8 solutions using aacu_instances (but, here, + there are infinitely many different solutions). We miss e.g. [a*a +b*a + + (x*x + y*x)*c], which seems to be more peculiar. *) + aacu_instances <- H. + + (** The 7 last solutions are the same as if we were matching [1] *) + aacu_instances H1. Abort. + +(** The behavior of the tactic is not satisfying in this case. It is +still unclear how to handle properly this kind of situation : we plan +to investigate on this in the future *) + +End Z. + diff --git a/theories/Instances.v b/theories/Instances.v new file mode 100644 index 0000000..d007ceb --- /dev/null +++ b/theories/Instances.v @@ -0,0 +1,261 @@ +(***************************************************************************) +(* This is part of aac_tactics, it is distributed under the terms of the *) +(* GNU Lesser General Public License version 3 *) +(* (see file LICENSE for more details) *) +(* *) +(* Copyright 2009-2010: Thomas Braibant, Damien Pous. *) +(***************************************************************************) + +Require List. +Require Arith NArith Max Min. +Require ZArith Zminmax. +Require QArith Qminmax. +Require Relations. + +From AAC_tactics +Require Export AAC. + +(** Instances for aac_rewrite.*) + + +(* This one is not declared as an instance: this interferes badly with setoid_rewrite *) +Lemma eq_subr {X} {R} `{@Reflexive X R}: subrelation eq R. +Proof. intros x y ->. reflexivity. Qed. + +(* At the moment, all the instances are exported even if they are packaged into modules. Even using LocalInstances in fact*) + +Module Peano. + Import Arith NArith Max Min. + Instance aac_plus_Assoc : Associative eq plus := plus_assoc. + Instance aac_plus_Comm : Commutative eq plus := plus_comm. + + Instance aac_mult_Comm : Commutative eq mult := mult_comm. + Instance aac_mult_Assoc : Associative eq mult := mult_assoc. + + Instance aac_min_Comm : Commutative eq min := min_comm. + Instance aac_min_Assoc : Associative eq min := min_assoc. + + Instance aac_max_Comm : Commutative eq max := max_comm. + Instance aac_max_Assoc : Associative eq max := max_assoc. + + Instance aac_one : Unit eq mult 1 := Build_Unit eq mult 1 mult_1_l mult_1_r. + Instance aac_zero_plus : Unit eq plus O := Build_Unit eq plus (O) plus_0_l plus_0_r. + Instance aac_zero_max : Unit eq max O := Build_Unit eq max 0 max_0_l max_0_r. + + + (* We also provide liftings from le to eq *) + Instance preorder_le : PreOrder le := Build_PreOrder _ le_refl le_trans. + Instance lift_le_eq : AAC_lift le eq := Build_AAC_lift eq_equivalence _. + +End Peano. + + +Module Z. + Import ZArith Zminmax. + Open Scope Z_scope. + Instance aac_Zplus_Assoc : Associative eq Zplus := Zplus_assoc. + Instance aac_Zplus_Comm : Commutative eq Zplus := Zplus_comm. + + Instance aac_Zmult_Comm : Commutative eq Zmult := Zmult_comm. + Instance aac_Zmult_Assoc : Associative eq Zmult := Zmult_assoc. + + Instance aac_Zmin_Comm : Commutative eq Z.min := Z.min_comm. + Instance aac_Zmin_Assoc : Associative eq Z.min := Z.min_assoc. + + Instance aac_Zmax_Comm : Commutative eq Z.max := Z.max_comm. + Instance aac_Zmax_Assoc : Associative eq Z.max := Z.max_assoc. + + Instance aac_one : Unit eq Zmult 1 := Build_Unit eq Zmult 1 Zmult_1_l Zmult_1_r. + Instance aac_zero_Zplus : Unit eq Zplus 0 := Build_Unit eq Zplus 0 Zplus_0_l Zplus_0_r. + + (* We also provide liftings from le to eq *) + Instance preorder_Zle : PreOrder Z.le := Build_PreOrder _ Z.le_refl Z.le_trans. + Instance lift_le_eq : AAC_lift Z.le eq := Build_AAC_lift eq_equivalence _. + +End Z. + +Module Lists. + Import List. + Instance aac_append_Assoc {A} : Associative eq (@app A) := @app_assoc A. + Instance aac_nil_append {A} : @Unit (list A) eq (@app A) (@nil A) := Build_Unit _ (@app A) (@nil A) (@app_nil_l A) (@app_nil_r A). + Instance aac_append_Proper {A} : Proper (eq ==> eq ==> eq) (@app A). + Proof. + repeat intro. + subst. + reflexivity. + Qed. +End Lists. + + +Module N. + Import NArith. + Open Scope N_scope. + Instance aac_Nplus_Assoc : Associative eq Nplus := Nplus_assoc. + Instance aac_Nplus_Comm : Commutative eq Nplus := Nplus_comm. + + Instance aac_Nmult_Comm : Commutative eq Nmult := Nmult_comm. + Instance aac_Nmult_Assoc : Associative eq Nmult := Nmult_assoc. + + Instance aac_Nmin_Comm : Commutative eq N.min := N.min_comm. + Instance aac_Nmin_Assoc : Associative eq N.min := N.min_assoc. + + Instance aac_Nmax_Comm : Commutative eq N.max := N.max_comm. + Instance aac_Nmax_Assoc : Associative eq N.max := N.max_assoc. + + Instance aac_one : Unit eq Nmult (1)%N := Build_Unit eq Nmult (1)%N Nmult_1_l Nmult_1_r. + Instance aac_zero : Unit eq Nplus (0)%N := Build_Unit eq Nplus (0)%N Nplus_0_l Nplus_0_r. + Instance aac_zero_max : Unit eq N.max 0 := Build_Unit eq N.max 0 N.max_0_l N.max_0_r. + + (* We also provide liftings from le to eq *) + Instance preorder_le : PreOrder N.le := Build_PreOrder N.le N.le_refl N.le_trans. + Instance lift_le_eq : AAC_lift N.le eq := Build_AAC_lift eq_equivalence _. + +End N. + +Module P. + Import NArith. + Open Scope positive_scope. + Instance aac_Pplus_Assoc : Associative eq Pplus := Pplus_assoc. + Instance aac_Pplus_Comm : Commutative eq Pplus := Pplus_comm. + + Instance aac_Pmult_Comm : Commutative eq Pmult := Pmult_comm. + Instance aac_Pmult_Assoc : Associative eq Pmult := Pmult_assoc. + + Instance aac_Pmin_Comm : Commutative eq Pos.min := Pos.min_comm. + Instance aac_Pmin_Assoc : Associative eq Pos.min := Pos.min_assoc. + + Instance aac_Pmax_Comm : Commutative eq Pos.max := Pos.max_comm. + Instance aac_Pmax_Assoc : Associative eq Pos.max := Pos.max_assoc. + + Instance aac_one : Unit eq Pmult 1 := Build_Unit eq Pmult 1 _ Pmult_1_r. + intros; reflexivity. Qed. (* TODO : add this lemma in the stdlib *) + Instance aac_one_max : Unit eq Pos.max 1 := Build_Unit eq Pos.max 1 Pos.max_1_l Pos.max_1_r. + + (* We also provide liftings from le to eq *) + Instance preorder_le : PreOrder Pos.le := Build_PreOrder Pos.le Pos.le_refl Pos.le_trans. + Instance lift_le_eq : AAC_lift Pos.le eq := Build_AAC_lift eq_equivalence _. +End P. + +Module Q. + Import QArith Qminmax. + Instance aac_Qplus_Assoc : Associative Qeq Qplus := Qplus_assoc. + Instance aac_Qplus_Comm : Commutative Qeq Qplus := Qplus_comm. + + Instance aac_Qmult_Comm : Commutative Qeq Qmult := Qmult_comm. + Instance aac_Qmult_Assoc : Associative Qeq Qmult := Qmult_assoc. + + Instance aac_Qmin_Comm : Commutative Qeq Qmin := Q.min_comm. + Instance aac_Qmin_Assoc : Associative Qeq Qmin := Q.min_assoc. + + Instance aac_Qmax_Comm : Commutative Qeq Qmax := Q.max_comm. + Instance aac_Qmax_Assoc : Associative Qeq Qmax := Q.max_assoc. + + Instance aac_one : Unit Qeq Qmult 1 := Build_Unit Qeq Qmult 1 Qmult_1_l Qmult_1_r. + Instance aac_zero_Qplus : Unit Qeq Qplus 0 := Build_Unit Qeq Qplus 0 Qplus_0_l Qplus_0_r. + + (* We also provide liftings from le to eq *) + Instance preorder_le : PreOrder Qle := Build_PreOrder Qle Qle_refl Qle_trans. + Instance lift_le_eq : AAC_lift Qle Qeq := Build_AAC_lift QOrderedType.QOrder.TO.eq_equiv _. + +End Q. + +Module Prop_ops. + Instance aac_or_Assoc : Associative iff or. Proof. unfold Associative; tauto. Qed. + Instance aac_or_Comm : Commutative iff or. Proof. unfold Commutative; tauto. Qed. + Instance aac_and_Assoc : Associative iff and. Proof. unfold Associative; tauto. Qed. + Instance aac_and_Comm : Commutative iff and. Proof. unfold Commutative; tauto. Qed. + Instance aac_True : Unit iff or False. Proof. constructor; firstorder. Qed. + Instance aac_False : Unit iff and True. Proof. constructor; firstorder. Qed. + + Program Instance aac_not_compat : Proper (iff ==> iff) not. + Solve All Obligations with firstorder. + + Instance lift_impl_iff : AAC_lift Basics.impl iff := Build_AAC_lift _ _. +End Prop_ops. + +Module Bool. + Instance aac_orb_Assoc : Associative eq orb. Proof. unfold Associative; firstorder. Qed. + Instance aac_orb_Comm : Commutative eq orb. Proof. unfold Commutative; firstorder. Qed. + Instance aac_andb_Assoc : Associative eq andb. Proof. unfold Associative; firstorder. Qed. + Instance aac_andb_Comm : Commutative eq andb. Proof. unfold Commutative; firstorder. Qed. + Instance aac_true : Unit eq orb false. Proof. constructor; firstorder. Qed. + Instance aac_false : Unit eq andb true. Proof. constructor; intros [|];firstorder. Qed. + + Instance negb_compat : Proper (eq ==> eq) negb. Proof. intros [|] [|]; auto. Qed. +End Bool. + +Module Relations. + Import Relations.Relations. + Section defs. + Variable T : Type. + Variables R S: relation T. + Definition inter : relation T := fun x y => R x y /\ S x y. + Definition compo : relation T := fun x y => exists z : T, R x z /\ S z y. + Definition negr : relation T := fun x y => ~ R x y. + (* union and converse are already defined in the standard library *) + + Definition bot : relation T := fun _ _ => False. + Definition top : relation T := fun _ _ => True. + End defs. + + Instance eq_same_relation T : Equivalence (same_relation T). Proof. firstorder. Qed. + + Instance aac_union_Comm T : Commutative (same_relation T) (union T). Proof. unfold Commutative; compute; intuition. Qed. + Instance aac_union_Assoc T : Associative (same_relation T) (union T). Proof. unfold Associative; compute; intuition. Qed. + Instance aac_bot T : Unit (same_relation T) (union T) (bot T). Proof. constructor; compute; intuition. Qed. + + Instance aac_inter_Comm T : Commutative (same_relation T) (inter T). Proof. unfold Commutative; compute; intuition. Qed. + Instance aac_inter_Assoc T : Associative (same_relation T) (inter T). Proof. unfold Associative; compute; intuition. Qed. + Instance aac_top T : Unit (same_relation T) (inter T) (top T). Proof. constructor; compute; intuition. Qed. + + (* note that we use [eq] directly as a neutral element for composition *) + Instance aac_compo T : Associative (same_relation T) (compo T). Proof. unfold Associative; compute; firstorder. Qed. + Instance aac_eq T : Unit (same_relation T) (compo T) (eq). Proof. compute; firstorder subst; trivial. Qed. + + Instance negr_compat T : Proper (same_relation T ==> same_relation T) (negr T). + Proof. compute. firstorder. Qed. + + Instance transp_compat T : Proper (same_relation T ==> same_relation T) (transp T). + Proof. compute. firstorder. Qed. + + Instance clos_trans_incr T : Proper (inclusion T ==> inclusion T) (clos_trans T). + Proof. + intros R S H x y Hxy. induction Hxy. + constructor 1. apply H. assumption. + econstructor 2; eauto 3. + Qed. + Instance clos_trans_compat T: Proper (same_relation T ==> same_relation T) (clos_trans T). + Proof. intros R S H; split; apply clos_trans_incr, H. Qed. + + Instance clos_refl_trans_incr T : Proper (inclusion T ==> inclusion T) (clos_refl_trans T). + Proof. + intros R S H x y Hxy. induction Hxy. + constructor 1. apply H. assumption. + constructor 2. + econstructor 3; eauto 3. + Qed. + Instance clos_refl_trans_compat T : Proper (same_relation T ==> same_relation T) (clos_refl_trans T). + Proof. intros R S H; split; apply clos_refl_trans_incr, H. Qed. + + Instance preorder_inclusion T : PreOrder (inclusion T). + Proof. constructor; unfold Reflexive, Transitive, inclusion; intuition. Qed. + + Instance lift_inclusion_same_relation T: AAC_lift (inclusion T) (same_relation T) := + Build_AAC_lift (eq_same_relation T) _. + Proof. firstorder. Qed. + +End Relations. + +Module All. + Export Peano. + Export Z. + Export P. + Export N. + Export Prop_ops. + Export Bool. + Export Relations. +End All. + +(* Here, we should not see any instance of our classes. + Print HintDb typeclass_instances. +*) diff --git a/theories/Tutorial.v b/theories/Tutorial.v new file mode 100644 index 0000000..e403d92 --- /dev/null +++ b/theories/Tutorial.v @@ -0,0 +1,401 @@ +(***************************************************************************) +(* This is part of aac_tactics, it is distributed under the terms of the *) +(* GNU Lesser General Public License version 3 *) +(* (see file LICENSE for more details) *) +(* *) +(* Copyright 2009-2010: Thomas Braibant, Damien Pous. *) +(***************************************************************************) + +(** * Tutorial for using the [aac_tactics] library. + + Depending on your installation, either modify the following two + lines, or add them to your .coqrc files, replacing "." with the + path to the [aac_tactics] library. *) + +Require Arith ZArith. + +From AAC_tactics +Require Import AAC. +From AAC_tactics +Require Instances. + +(** ** Introductory example + + Here is a first example with relative numbers ([Z]): one can + rewrite an universally quantified hypothesis modulo the + associativity and commutativity of [Zplus]. *) + +Section introduction. + + Import ZArith. + Import Instances.Z. + + Variables a b c : Z. + Hypothesis H: forall x, x + Z.opp x = 0. + Goal a + b + c + Z.opp (c + a) = b. + aac_rewrite H. + aac_reflexivity. + Qed. + Goal a + c + Z.opp (b + a + Z.opp b) = c. + do 2 aac_rewrite H. + reflexivity. + Qed. + + (** Notes: + - the tactic handles arbitrary function symbols like [Zopp] (as + long as they are proper morphisms w.r.t. the considered + equivalence relation); + - here, ring would have done the job. + *) + +End introduction. + + +(** ** Usage + + One can also work in an abstract context, with arbitrary + associative and commutative operators. (Note that one can declare + several operations of each kind.) *) + +Section base. + Context {X} {R} {E: Equivalence R} + {plus} + {dot} + {zero} + {one} + {dot_A: @Associative X R dot } + {plus_A: @Associative X R plus } + {plus_C: @Commutative X R plus } + {dot_Proper :Proper (R ==> R ==> R) dot} + {plus_Proper :Proper (R ==> R ==> R) plus} + {Zero : Unit R plus zero} + {One : Unit R dot one} + . + + Notation "x == y" := (R x y) (at level 70). + Notation "x * y" := (dot x y) (at level 40, left associativity). + Notation "1" := (one). + Notation "x + y" := (plus x y) (at level 50, left associativity). + Notation "0" := (zero). + + (** In the very first example, [ring] would have solved the + goal. Here, since [dot] does not necessarily distribute over [plus], + it is not possible to rely on it. *) + + Section reminder. + Hypothesis H : forall x, x * x == x. + Variables a b c : X. + + Goal (a+b+c)*(c+a+b) == a+b+c. + aac_rewrite H. + aac_reflexivity. + Qed. + + (** The tactic starts by normalising terms, so that trailing units + are always eliminated. *) + + Goal ((a+b)+0+c)*((c+a)+b*1) == a+b+c. + aac_rewrite H. + aac_reflexivity. + Qed. + End reminder. + + (** The tactic can deal with "proper" morphisms of arbitrary arity + (here [f] and [g], or [Zopp] earlier): it rewrites under such + morphisms ([g]), and, more importantly, it is able to reorder + terms modulo AC under these morphisms ([f]). *) + + Section morphisms. + Variable f : X -> X -> X. + Hypothesis Hf : Proper (R ==> R ==> R) f. + Variable g : X -> X. + Hypothesis Hg : Proper (R ==> R) g. + + Variable a b: X. + Hypothesis H : forall x y, x+f (b+y) x == y+x. + Goal g ((f (a+b) a) + a) == g (a+a). + aac_rewrite H. + reflexivity. + Qed. + End morphisms. + + (** *** Selecting what and where to rewrite + + There are sometimes several solutions to the matching problem. We + now show how to interact with the tactic to select the desired + one. *) + + Section occurrence. + Variable f : X -> X. + Variable a : X. + Hypothesis Hf : Proper (R ==> R) f. + Hypothesis H : forall x, x + x == x. + + Goal f(a+a)+f(a+a) == f a. + (** In case there are several possible solutions, one can print + the different solutions using the [aac_instances] tactic (in + proof-general, look at buffer *coq* ): *) + aac_instances H. + (** the default choice is the occurrence with the smallest + possible context (number 0), but one can choose the desired + one; *) + aac_rewrite H at 1. + (** now the goal is [f a + f a == f a], there is only one solution. *) + aac_rewrite H. + reflexivity. + Qed. + + End occurrence. + + Section subst. + Variables a b c d : X. + Hypothesis H: forall x y, a*x*y*b == a*(x+y)*b. + Hypothesis H': forall x, x + x == x. + + Goal a*c*d*c*d*b == a*c*d*b. + (** Here, there is only one possible occurrence, but several substitutions; *) + aac_instances H. + (** one can select them with the proper keyword. *) + aac_rewrite H subst 1. + aac_rewrite H'. + aac_reflexivity. + Qed. + End subst. + + (** As expected, one can use both keywords together to select the + occurrence and the substitution. We also provide a keyword to + specify that the rewrite should be done in the right-hand side of + the equation. *) + + Section both. + Variables a b c d : X. + Hypothesis H: forall x y, a*x*y*b == a*(x+y)*b. + Hypothesis H': forall x, x + x == x. + + Goal a*c*d*c*d*b*b == a*(c*d*b)*b. + aac_instances H. + aac_rewrite H at 1 subst 1. + aac_instances H. + aac_rewrite H. + aac_rewrite H'. + aac_rewrite H at 0 subst 1 in_right. + aac_reflexivity. + Qed. + + End both. + + (** *** Distinction between [aac_rewrite] and [aacu_rewrite]: + + [aac_rewrite] rejects solutions in which variables are instantiated + by units, while the companion tactic, [aacu_rewrite] allows such + solutions. *) + + Section dealing_with_units. + Variables a b c: X. + Hypothesis H: forall x, a*x*a == x. + Goal a*a == 1. + (** Here, [x] must be instantiated with [1], so that the [aac_*] + tactics give no solutions; *) + try aac_instances H. + (** while we get solutions with the [aacu_*] tactics. *) + aacu_instances H. + aacu_rewrite H. + reflexivity. + Qed. + + (** We introduced this distinction because it allows us to rule + out dummy cases in common situations: *) + + Hypothesis H': forall x y z, x*y + x*z == x*(y+z). + Goal a*b*c + a*c + a*b == a*(c+b*(1+c)). + (** 6 solutions without units, *) + aac_instances H'. + aac_rewrite H' at 0. + (** more than 52 with units. *) + aacu_instances H'. + Abort. + + End dealing_with_units. +End base. + +(** *** Declaring instances + + To use one's own operations: it suffices to declare them as + instances of our classes. (Note that the following instances are + already declared in file [Instances.v].) *) + +Section Peano. + Import Arith. + + Instance aac_plus_Assoc : Associative eq plus := plus_assoc. + Instance aac_plus_Comm : Commutative eq plus := plus_comm. + + Instance aac_one : Unit eq mult 1 := + Build_Unit eq mult 1 mult_1_l mult_1_r. + Instance aac_zero_plus : Unit eq plus O := + Build_Unit eq plus (O) plus_0_l plus_0_r. + + + (** Two (or more) operations may share the same units: in the + following example, [0] is understood as the unit of [max] as well as + the unit of [plus]. *) + + Instance aac_max_Comm : Commutative eq Max.max := Max.max_comm. + Instance aac_max_Assoc : Associative eq Max.max := Max.max_assoc. + + Instance aac_zero_max : Unit eq Max.max O := + Build_Unit eq Max.max 0 Max.max_0_l Max.max_0_r. + + Variable a b c : nat. + Goal Max.max (a + 0) 0 = a. + aac_reflexivity. + Qed. + + (** Furthermore, several operators can be mixed: *) + + Hypothesis H : forall x y z, Max.max (x + y) (x + z) = x+ Max.max y z. + + Goal Max.max (a + b) (c + (a * 1)) = Max.max c b + a. + aac_instances H. aac_rewrite H. aac_reflexivity. + Qed. + Goal Max.max (a + b) (c + Max.max (a*1+0) 0) = a + Max.max b c. + aac_instances H. aac_rewrite H. aac_reflexivity. + Qed. + + + (** *** Working with inequations + + To be able to use the tactics, the goal must be a relation [R] + applied to two arguments, and the rewritten hypothesis must end + with a relation [Q] applied to two arguments. These relations are + not necessarily equivalences, but they should be related + according to the occurrence where the rewrite takes place; we + leave this check to the underlying call to [setoid_rewrite]. *) + + (** One can rewrite equations in the left member of inequations, *) + Goal (forall x, x + x = x) -> a + b + b + a <= a + b. + intro Hx. + aac_rewrite Hx. + reflexivity. + Qed. + + (** or in the right member of inequations, using the [in_right] keyword *) + Goal (forall x, x + x = x) -> a + b <= a + b + b + a. + intro Hx. + aac_rewrite Hx in_right. + reflexivity. + Qed. + + (** Similarly, one can rewrite inequations in inequations, *) + Goal (forall x, x + x <= x) -> a + b + b + a <= a + b. + intro Hx. + aac_rewrite Hx. + reflexivity. + Qed. + + (** possibly in the right-hand side. *) + Goal (forall x, x <= x + x) -> a + b <= a + b + b + a. + intro Hx. + aac_rewrite <- Hx in_right. + reflexivity. + Qed. + + (** [aac_reflexivity] deals with "trivial" inequations too *) + Goal Max.max (a + b) (c + a) <= Max.max (b + a) (c + 1*a). + aac_reflexivity. + Qed. + + (** In the last three examples, there were no equivalence relation + involved in the goal. However, we actually had to guess the + equivalence relation with respect to which the operators + ([plus,max,0]) were AC. In this case, it was Leibniz equality + [eq] so that it was automatically inferred; more generally, one + can specify which equivalence relation to use by declaring + instances of the [AAC_lift] type class: *) + + Instance lift_le_eq : AAC_lift le eq := {}. + (** (This instance is automatically inferred because [eq] is always a + valid candidate, here for [le].) *) + + +End Peano. + + +(** *** Normalising goals + + We also provide a tactic to normalise terms modulo AC. This + normalisation is the one we use internally. *) + +Section AAC_normalise. + + Import Instances.Z. + Import ZArith. + Open Scope Z_scope. + + Variable a b c d : Z. + Goal a + (b + c*c*d) + a + 0 + d*1 = a. + aac_normalise. + Abort. + +End AAC_normalise. + + + + +(** ** Examples from the web page *) +Section Examples. + + Import Instances.Z. + Import ZArith. + Open Scope Z_scope. + + (** *** Reverse triangle inequality *) + + Lemma Zabs_triangle : forall x y, Z.abs (x + y) <= Z.abs x + Z.abs y . + Proof Z.abs_triangle. + + Lemma Zplus_opp_r : forall x, x + -x = 0. + Proof Zplus_opp_r. + + (** The following morphisms are required to perform the required rewrites *) + Instance Zminus_compat : Proper (Z.ge ==> Z.le) Z.opp. + Proof. intros x y. omega. Qed. + + Instance Proper_Zplus : Proper (Z.le ==> Z.le ==> Z.le) Zplus. + Proof. firstorder. Qed. + + Goal forall a b, Z.abs a - Z.abs b <= Z.abs (a - b). + intros. unfold Zminus. + aac_instances <- (Zminus_diag b). + aac_rewrite <- (Zminus_diag b) at 3. + unfold Zminus. + aac_rewrite Z.abs_triangle. + aac_rewrite Zplus_opp_r. + aac_reflexivity. + Qed. + + + (** *** Pythagorean triples *) + + Notation "x ^2" := (x*x) (at level 40). + Notation "2 ⋅ x" := (x+x) (at level 41). + + Lemma Hbin1: forall x y, (x+y)^2 = x^2 + y^2 + 2⋅x*y. Proof. intros; ring. Qed. + Lemma Hbin2: forall x y, x^2 + y^2 = (x+y)^2 + -(2⋅x*y). Proof. intros; ring. Qed. + Lemma Hopp : forall x, x + -x = 0. Proof Zplus_opp_r. + + Variables a b c : Z. + Hypothesis H : c^2 + 2⋅(a+1)*b = (a+1+b)^2. + Goal a^2 + b^2 + 2⋅a + 1 = c^2. + aacu_rewrite <- Hbin1. + rewrite Hbin2. + aac_rewrite <- H. + aac_rewrite Hopp. + aac_reflexivity. + Qed. + + (** Note: after the [aac_rewrite <- H], one could use [ring] to close the proof.*) + +End Examples. + + diff --git a/theories/Utils.v b/theories/Utils.v new file mode 100644 index 0000000..0f37ae1 --- /dev/null +++ b/theories/Utils.v @@ -0,0 +1,257 @@ +(***************************************************************************) +(* This is part of aac_tactics, it is distributed under the terms of the *) +(* GNU Lesser General Public License version 3 *) +(* (see file LICENSE for more details) *) +(* *) +(* Copyright 2009-2010: Thomas Braibant, Damien Pous. *) +(***************************************************************************) + + +Require Import Arith NArith. +Require Import List. +Require Import FMapPositive FMapFacts. +Require Import RelationClasses Equality. + +Set Implicit Arguments. +Set Asymmetric Patterns. + +(** * Utilities for positive numbers + which we use as: + - indices for morphisms and symbols + - multiplicity of terms in sums *) + +Notation idx := positive. + +Fixpoint eq_idx_bool i j := + match i,j with + | xH, xH => true + | xO i, xO j => eq_idx_bool i j + | xI i, xI j => eq_idx_bool i j + | _, _ => false + end. + +Fixpoint idx_compare i j := + match i,j with + | xH, xH => Eq + | xH, _ => Lt + | _, xH => Gt + | xO i, xO j => idx_compare i j + | xI i, xI j => idx_compare i j + | xI _, xO _ => Gt + | xO _, xI _ => Lt + end. + +Notation pos_compare := idx_compare (only parsing). + +(** Specification predicate for boolean binary functions *) +Inductive decide_spec {A} {B} (R : A -> B -> Prop) (x : A) (y : B) : bool -> Prop := +| decide_true : R x y -> decide_spec R x y true +| decide_false : ~(R x y) -> decide_spec R x y false. + +Lemma eq_idx_spec : forall i j, decide_spec (@eq _) i j (eq_idx_bool i j). +Proof. + induction i; destruct j; simpl; try (constructor; congruence). + case (IHi j); constructor; congruence. + case (IHi j); constructor; congruence. +Qed. + +(** weak specification predicate for comparison functions: only the 'Eq' case is specified *) +Inductive compare_weak_spec A: A -> A -> comparison -> Prop := +| pcws_eq: forall i, compare_weak_spec i i Eq +| pcws_lt: forall i j, compare_weak_spec i j Lt +| pcws_gt: forall i j, compare_weak_spec i j Gt. + +Lemma pos_compare_weak_spec: forall i j, compare_weak_spec i j (pos_compare i j). +Proof. induction i; destruct j; simpl; try constructor; case (IHi j); intros; constructor. Qed. + +Lemma idx_compare_reflect_eq: forall i j, idx_compare i j = Eq -> i=j. +Proof. intros i j. case (pos_compare_weak_spec i j); intros; congruence. Qed. + +(** * Dependent types utilities *) + +Notation cast T H u := (eq_rect _ T u _ H). + +Section dep. + Variable U: Type. + Variable T: U -> Type. + + Lemma cast_eq: (forall u v: U, {u=v}+{u<>v}) -> + forall A (H: A=A) (u: T A), cast T H u = u. + Proof. intros. rewrite <- Eqdep_dec.eq_rect_eq_dec; trivial. Qed. + + Variable f: forall A B, T A -> T B -> comparison. + Definition reflect_eqdep := forall A u B v (H: A=B), @f A B u v = Eq -> cast T H u = v. + + (* these lemmas have to remain transparent to get structural recursion + in the lemma [tcompare_weak_spec] below *) + Lemma reflect_eqdep_eq: reflect_eqdep -> + forall A u v, @f A A u v = Eq -> u = v. + Proof. intros H A u v He. apply (H _ _ _ _ eq_refl He). Defined. + + Lemma reflect_eqdep_weak_spec: reflect_eqdep -> + forall A u v, compare_weak_spec u v (@f A A u v). + Proof. + intros. case_eq (f u v); try constructor. + intro H'. apply reflect_eqdep_eq in H'. subst. constructor. assumption. + Defined. +End dep. + + +(** * Utilities about (non-empty) lists and multisets *) + +Inductive nelist (A : Type) : Type := +| nil : A -> nelist A +| cons : A -> nelist A -> nelist A. + +Notation "x :: y" := (cons x y). + +Fixpoint nelist_map (A B: Type) (f: A -> B) l := + match l with + | nil x => nil ( f x) + | cons x l => cons ( f x) (nelist_map f l) + end. + +Fixpoint appne A l l' : nelist A := + match l with + nil x => cons x l' + | cons t q => cons t (appne A q l') + end. + +Notation "x ++ y" := (appne x y). + +(** finite multisets are represented with ordered lists with multiplicities *) +Definition mset A := nelist (A*positive). + +(** lexicographic composition of comparisons (this is a notation to keep it lazy) *) +Notation lex e f := (match e with Eq => f | _ => e end). + + +Section lists. + + (** comparison functions *) + + Section c. + Variables A B: Type. + Variable compare: A -> B -> comparison. + Fixpoint list_compare h k := + match h,k with + | nil x, nil y => compare x y + | nil x, _ => Lt + | _, nil x => Gt + | u::h, v::k => lex (compare u v) (list_compare h k) + end. + End c. + Definition mset_compare A B compare: mset A -> mset B -> comparison := + list_compare (fun un vm => + let '(u,n) := un in + let '(v,m) := vm in + lex (compare u v) (pos_compare n m)). + + Section list_compare_weak_spec. + Variable A: Type. + Variable compare: A -> A -> comparison. + Hypothesis Hcompare: forall u v, compare_weak_spec u v (compare u v). + (* this lemma has to remain transparent to get structural recursion + in the lemma [tcompare_weak_spec] below *) + Lemma list_compare_weak_spec: forall h k, + compare_weak_spec h k (list_compare compare h k). + Proof. + induction h as [|u h IHh]; destruct k as [|v k]; simpl; try constructor. + + case (Hcompare a a0 ); try constructor. + case (Hcompare u v ); try constructor. + case (IHh k); intros; constructor. + Defined. + End list_compare_weak_spec. + + Section mset_compare_weak_spec. + Variable A: Type. + Variable compare: A -> A -> comparison. + Hypothesis Hcompare: forall u v, compare_weak_spec u v (compare u v). + (* this lemma has to remain transparent to get structural recursion + in the lemma [tcompare_weak_spec] below *) + Lemma mset_compare_weak_spec: forall h k, + compare_weak_spec h k (mset_compare compare h k). + Proof. + apply list_compare_weak_spec. + intros [u n] [v m]. + case (Hcompare u v); try constructor. + case (pos_compare_weak_spec n m); try constructor. + Defined. + End mset_compare_weak_spec. + + (** (sorted) merging functions *) + + Section m. + Variable A: Type. + Variable compare: A -> A -> comparison. + Definition insert n1 h1 := + let fix insert_aux l2 := + match l2 with + | nil (h2,n2) => + match compare h1 h2 with + | Eq => nil (h1,Pplus n1 n2) + | Lt => (h1,n1):: nil (h2,n2) + | Gt => (h2,n2):: nil (h1,n1) + end + | (h2,n2)::t2 => + match compare h1 h2 with + | Eq => (h1,Pplus n1 n2):: t2 + | Lt => (h1,n1)::l2 + | Gt => (h2,n2)::insert_aux t2 + end + end + in insert_aux. + + Fixpoint merge_msets l1 := + match l1 with + | nil (h1,n1) => fun l2 => insert n1 h1 l2 + | (h1,n1)::t1 => + let fix merge_aux l2 := + match l2 with + | nil (h2,n2) => + match compare h1 h2 with + | Eq => (h1,Pplus n1 n2) :: t1 + | Lt => (h1,n1):: merge_msets t1 l2 + | Gt => (h2,n2):: l1 + end + | (h2,n2)::t2 => + match compare h1 h2 with + | Eq => (h1,Pplus n1 n2)::merge_msets t1 t2 + | Lt => (h1,n1)::merge_msets t1 l2 + | Gt => (h2,n2)::merge_aux t2 + end + end + in merge_aux + end. + + (** interpretation of a list with a constant and a binary operation *) + + Variable B: Type. + Variable map: A -> B. + Variable b2: B -> B -> B. + Fixpoint fold_map l := + match l with + | nil x => map x + | u::l => b2 (map u) (fold_map l) + end. + + (** mapping and merging *) + + Variable merge: A -> nelist B -> nelist B. + Fixpoint merge_map (l: nelist A): nelist B := + match l with + | nil x => nil (map x) + | u::l => merge u (merge_map l) + end. + + Variable ret : A -> B. + Variable bind : A -> B -> B. + Fixpoint fold_map' (l : nelist A) : B := + match l with + | nil x => ret x + | u::l => bind u (fold_map' l) + end. + + End m. +End lists. -- cgit v1.2.3