From b9314c345ddc958021a5262df369d6e2598b5340 Mon Sep 17 00:00:00 2001 From: Michael Sippel Date: Thu, 19 Sep 2024 21:15:43 +0200 Subject: [PATCH] take over FiniteSet & Atom libraries from popl-tutorial --- coq/AdditionalTactics.v | 109 +++++++++++++++ coq/Atom.v | 265 +++++++++++++++++++++++++++++++++++ coq/FSetNotin.v | 185 +++++++++++++++++++++++++ coq/FiniteSets.v | 65 +++++++++ coq/ListFacts.v | 299 ++++++++++++++++++++++++++++++++++++++++ coq/_CoqProject | 5 + 6 files changed, 928 insertions(+) create mode 100644 coq/AdditionalTactics.v create mode 100644 coq/Atom.v create mode 100644 coq/FSetNotin.v create mode 100644 coq/FiniteSets.v create mode 100644 coq/ListFacts.v diff --git a/coq/AdditionalTactics.v b/coq/AdditionalTactics.v new file mode 100644 index 0000000..ff2d7cf --- /dev/null +++ b/coq/AdditionalTactics.v @@ -0,0 +1,109 @@ +(** A library of additional tactics. *) + +Require Export String. +Open Scope string_scope. + + +(* *********************************************************************** *) +(** * Extensions of the standard library *) + +(** "[remember c as x in |-]" replaces the term [c] by the identifier + [x] in the conclusion of the current goal and introduces the + hypothesis [x=c] into the context. This tactic differs from a + similar one in the standard library in that the replacmement is + made only in the conclusion of the goal; the context is left + unchanged. *) + +Tactic Notation "remember" constr(c) "as" ident(x) "in" "|-" := + let x := fresh x in + let H := fresh "Heq" x in + (set (x := c); assert (H : x = c) by reflexivity; clearbody x). + +(** "[unsimpl E]" replaces all occurence of [X] by [E], where [X] is + the result that tactic [simpl] would give when used to evaluate + [E]. *) + +Tactic Notation "unsimpl" constr(E) := + let F := (eval simpl in E) in change F with E. + +(** The following tactic calls the [apply] tactic with the first + hypothesis that succeeds, "first" meaning the hypothesis that + comes earlist in the context (i.e., higher up in the list). *) + +Ltac apply_first_hyp := + match reverse goal with + | H : _ |- _ => apply H + end. + + +(* *********************************************************************** *) +(** * Variations on [auto] *) + +(** The [auto*] and [eauto*] tactics are intended to be "stronger" + versions of the [auto] and [eauto] tactics. Similar to [auto] and + [eauto], they each take an optional "depth" argument. Note that + if we declare these tactics using a single string, e.g., "auto*", + then the resulting tactics are unusable since they fail to + parse. *) + +Tactic Notation "auto" "*" := + try solve [ congruence | auto | intuition auto ]. + +Tactic Notation "auto" "*" integer(n) := + try solve [ congruence | auto n | intuition (auto n) ]. + +Tactic Notation "eauto" "*" := + try solve [ congruence | eauto | intuition eauto ]. + +Tactic Notation "eauto" "*" integer(n) := + try solve [ congruence | eauto n | intuition (eauto n) ]. + + +(* *********************************************************************** *) +(** * Delineating cases in proofs *) + +(** This section was taken from the POPLmark Wiki + ( http://alliance.seas.upenn.edu/~plclub/cgi-bin/poplmark/ ). *) + +(** ** Tactic definitions *) + +Ltac move_to_top x := + match reverse goal with + | H : _ |- _ => try move x after H + end. + +Tactic Notation "assert_eq" ident(x) constr(v) := + let H := fresh in + assert (x = v) as H by reflexivity; + clear H. + +Tactic Notation "Case_aux" ident(x) constr(name) := + first [ + set (x := name); move_to_top x + | assert_eq x name + | fail 1 "because we are working on a different case." ]. + +Ltac Case name := Case_aux case name. +Ltac SCase name := Case_aux subcase name. +Ltac SSCase name := Case_aux subsubcase name. + +(** ** Example + + One mode of use for the above tactics is to wrap Coq's [induction] + tactic such that automatically inserts "case" markers into each + branch of the proof. For example: + +<< + Tactic Notation "induction" "nat" ident(n) := + induction n; [ Case "O" | Case "S" ]. + Tactic Notation "sub" "induction" "nat" ident(n) := + induction n; [ SCase "O" | SCase "S" ]. + Tactic Notation "sub" "sub" "induction" "nat" ident(n) := + induction n; [ SSCase "O" | SSCase "S" ]. +>> + + If you use such customized versions of the induction tactics, then + the [Case] tactic will verify that you are working on the case + that you think you are. You may also use the [Case] tactic with + the standard version of [induction], in which case no verification + is done. *) diff --git a/coq/Atom.v b/coq/Atom.v new file mode 100644 index 0000000..14b2304 --- /dev/null +++ b/coq/Atom.v @@ -0,0 +1,265 @@ +(** Support for atoms, i.e., objects with decidable equality. We + provide here the ability to generate an atom fresh for any finite + collection, e.g., the lemma [atom_fresh_for_set], and a tactic to + pick an atom fresh for the current proof context. + + Authors: Arthur Charguéraud and Brian Aydemir. + + Implementation note: In older versions of Coq, [OrderedTypeEx] + redefines decimal constants to be integers and not natural + numbers. The following scope declaration is intended to address + this issue. In newer versions of Coq, the declaration should be + benign. *) + +Require Import List. +(*Require Import Max.*) +Require Import OrderedType. +Require Import OrderedTypeEx. +Open Scope nat_scope. + +Require Import FiniteSets. +Require Import FSetDecide. +Require Import FSetNotin. +Require Import ListFacts. +Require Import Psatz. + +Require Import AdditionalTactics. +Require AdditionalTactics. + +(* ********************************************************************** *) +(** * Definition *) + +(** Atoms are structureless objects such that we can always generate + one fresh from a finite collection. Equality on atoms is [eq] and + decidable. We use Coq's module system to make abstract the + implementation of atoms. The [Export AtomImpl] line below allows + us to refer to the type [atom] and its properties without having + to qualify everything with "[AtomImpl.]". *) + +Module Type ATOM. + + Parameter atom : Set. + + Parameter atom_fresh_for_list : + forall (xs : list atom), {x : atom | ~ List.In x xs}. + + Declare Module Atom_as_OT : UsualOrderedType with Definition t := atom. + + Parameter eq_atom_dec : forall x y : atom, {x = y} + {x <> y}. + +End ATOM. + +(** The implementation of the above interface is hidden for + documentation purposes. *) + +Module AtomImpl : ATOM. + + (* begin hide *) + + Definition atom := nat. + + Lemma max_lt_r : forall x y z, + x <= z -> x <= max y z. + Proof. + induction x. auto with arith. + induction y; auto with arith. + simpl. induction z. lia. auto with arith. + Qed. + + Lemma nat_list_max : forall (xs : list nat), + { n : nat | forall x, In x xs -> x <= n }. + Proof. + induction xs as [ | x xs [y H] ]. + (* case: nil *) + exists 0. inversion 1. + (* case: cons x xs *) + exists (max x y). intros z J. simpl in J. destruct J as [K | K]. + subst. auto with arith. + auto using max_lt_r. + Qed. + + Lemma atom_fresh_for_list : + forall (xs : list nat), { n : nat | ~ List.In n xs }. + Proof. + intros xs. destruct (nat_list_max xs) as [x H]. + exists (S x). intros J. lapply (H (S x)). lia. trivial. + Qed. + + Module Atom_as_OT := Nat_as_OT. + Module Facts := OrderedTypeFacts Atom_as_OT. + + Definition eq_atom_dec : forall x y : atom, {x = y} + {x <> y} := + Facts.eq_dec. + + (* end hide *) + +End AtomImpl. + +Export AtomImpl. + + +(* ********************************************************************** *) +(** * Finite sets of atoms *) + + +(* ********************************************************************** *) +(** ** Definitions *) + +Module AtomSet : FiniteSets.S with Module E := Atom_as_OT := + FiniteSets.Make Atom_as_OT. + +(** The type [atoms] is the type of finite sets of [atom]s. *) + +Notation atoms := AtomSet.F.t. + +(** Basic operations on finite sets of atoms are available, in the + remainder of this file, without qualification. We use [Import] + instead of [Export] in order to avoid unnecessary namespace + pollution. *) + +Import AtomSet.F. + +(** We instantiate two modules which provide useful lemmas and tactics + work working with finite sets of atoms. *) + +Module AtomSetDecide := FSetDecide.Decide AtomSet.F. +Module AtomSetNotin := FSetNotin.Notin AtomSet.F. + + +(* *********************************************************************** *) +(** ** Tactics for working with finite sets of atoms *) + +(** The tactic [fsetdec] is a general purpose decision procedure + for solving facts about finite sets of atoms. *) + +Ltac fsetdec := try apply AtomSet.eq_if_Equal; AtomSetDecide.fsetdec. + +(** The tactic [notin_simpl] simplifies all hypotheses of the form [(~ + In x F)], where [F] is constructed from the empty set, singleton + sets, and unions. *) + +Ltac notin_simpl := AtomSetNotin.notin_simpl_hyps. + +(** The tactic [notin_solve], solves goals of the form [(~ In x F)], + where [F] is constructed from the empty set, singleton sets, and + unions. The goal must be provable from hypothesis of the form + simplified by [notin_simpl]. *) + +Ltac notin_solve := AtomSetNotin.notin_solve. + + +(* *********************************************************************** *) +(** ** Lemmas for working with finite sets of atoms *) + +(** We make some lemmas about finite sets of atoms available without + qualification by using abbreviations. *) + +Notation eq_if_Equal := AtomSet.eq_if_Equal. +Notation notin_empty := AtomSetNotin.notin_empty. +Notation notin_singleton := AtomSetNotin.notin_singleton. +Notation notin_singleton_rw := AtomSetNotin.notin_singleton_rw. +Notation notin_union := AtomSetNotin.notin_union. + + +(* ********************************************************************** *) +(** * Additional properties *) + +(** One can generate an atom fresh for a given finite set of atoms. *) + +Lemma atom_fresh_for_set : forall L : atoms, { x : atom | ~ In x L }. +Proof. + intros L. destruct (atom_fresh_for_list (elements L)) as [a H]. + exists a. intros J. contradiction H. + rewrite <- InA_iff_In. auto using elements_1. +Qed. + + +(* ********************************************************************** *) +(** * Additional tactics *) + + +(* ********************************************************************** *) +(** ** ## Picking a fresh atom *) + +(** We define three tactics which, when combined, provide a simple + mechanism for picking a fresh atom. We demonstrate their use + below with an example, the [example_pick_fresh] tactic. + + [(gather_atoms_with F)] returns the union of [(F x)], where [x] + ranges over all objects in the context such that [(F x)] is + well typed. The return type of [F] should be [atoms]. The + complexity of this tactic is due to the fact that there is no + support in [Ltac] for folding a function over the context. *) + +Ltac gather_atoms_with F := + let rec gather V := + match goal with + | H: ?S |- _ => + let FH := constr:(F H) in + match V with + | empty => gather FH + | context [FH] => fail 1 + | _ => gather (union FH V) + end + | _ => V + end in + let L := gather empty in eval simpl in L. + +(** [(beautify_fset V)] takes a set [V] built as a union of finite + sets and returns the same set with empty sets removed and union + operations associated to the right. Duplicate sets are also + removed from the union. *) + +Ltac beautify_fset V := + let rec go Acc E := + match E with + | union ?E1 ?E2 => let Acc1 := go Acc E2 in go Acc1 E1 + | empty => Acc + | ?E1 => match Acc with + | empty => E1 + | context [E1] => Acc + | _ => constr:(union E1 Acc) + end + end + in go empty V. + +(** The tactic [(pick fresh Y for L)] takes a finite set of atoms [L] + and a fresh name [Y], and adds to the context an atom with name + [Y] and a proof that [(~ In Y L)], i.e., that [Y] is fresh for + [L]. The tactic will fail if [Y] is already declared in the + context. *) + +Tactic Notation "pick" "fresh" ident(Y) "for" constr(L) := + let Fr := fresh "Fr" in + let L := beautify_fset L in + (destruct (atom_fresh_for_set L) as [Y Fr]). + + +(* ********************************************************************** *) +(** ** Demonstration *) + +(** The [example_pick_fresh] tactic below illustrates the general + pattern for using the above three tactics to define a tactic which + picks a fresh atom. The pattern is as follows: + - Repeatedly invoke [gather_atoms_with], using functions with + different argument types each time. + - Union together the result of the calls, and invoke + [(pick fresh ... for ...)] with that union of sets. *) + +Ltac example_pick_fresh Y := + let A := gather_atoms_with (fun x : atoms => x) in + let B := gather_atoms_with (fun x : atom => singleton x) in + pick fresh Y for (union A B). + +Lemma example_pick_fresh_use : forall (x y z : atom) (L1 L2 L3: atoms), True. +(* begin show *) +Proof. + intros x y z L1 L2 L3. example_pick_fresh k. + + (** At this point in the proof, we have a new atom [k] and a + hypothesis [Fr : ~ In k (union L1 (union L2 (union L3 (union + (singleton x) (union (singleton y) (singleton z))))))]. *) + + trivial. +Qed. +(* end show *) diff --git a/coq/FSetNotin.v b/coq/FSetNotin.v new file mode 100644 index 0000000..3206527 --- /dev/null +++ b/coq/FSetNotin.v @@ -0,0 +1,185 @@ +(** Lemmas and tactics for working with and solving goals related to + non-membership in finite sets. The main tactic of interest here + is [notin_solve]. + + Authors: Arthur Charguéraud and Brian Aydemir. *) + +Set Implicit Arguments. +Require Import FSetInterface. +Require Import AdditionalTactics. +Require AdditionalTactics. + +(* *********************************************************************** *) +(** * Implementation *) + +Module Notin (X : FSetInterface.S). + +Import X. +Import AdditionalTactics. + +(* *********************************************************************** *) +(** ** Facts about set (non-)membership *) + +Lemma in_singleton : forall x, + In x (singleton x). +Proof. + intros. + apply singleton_2. + generalize dependent x. + apply E.eq_refl. +Qed. + +Lemma notin_empty : forall x, + ~ In x empty. +Proof. + auto using empty_1. +Qed. + +Lemma notin_union : forall x E F, + ~ In x E -> ~ In x F -> ~ In x (union E F). +Proof. + intros x E F H J K. + destruct (union_1 K); intuition. +Qed. + +Lemma elim_notin_union : forall x E F, + ~ In x (union E F) -> (~ In x E) /\ (~ In x F). +Proof. + intros x E F H. split; intros J; contradiction H. + auto using union_2. + auto using union_3. +Qed. + +Lemma notin_singleton : forall x y, + ~ E.eq x y -> ~ In x (singleton y). +Proof. + intros x y H J. assert (K := singleton_1 J). auto with *. +Qed. + +Lemma elim_notin_singleton : forall x y, + ~ In x (singleton y) -> ~ E.eq x y. +Proof. + intros x y H J. + contradiction H. + apply singleton_2. + generalize x y J. + apply E.eq_sym. +Qed. + +Lemma elim_notin_singleton' : forall x y, + ~ In x (singleton y) -> x <> y. +Proof. + intros. assert (~ E.eq x y). auto using singleton_2. + intros J. subst. auto with *. + contradict H0. + rewrite H0. + apply E.eq_refl. +Qed. + +Lemma notin_singleton_swap : forall x y, + ~ In x (singleton y) -> ~ In y (singleton x). +Proof. + intros. + assert (Q := elim_notin_singleton H). + auto using singleton_1. +Qed. + + +(* *********************************************************************** *) +(** ** Rewriting non-membership facts *) + +Lemma notin_singleton_rw : forall x y, + ~ In x (singleton y) <-> ~ E.eq x y. +Proof. + intros. split. + auto using elim_notin_singleton. + auto using notin_singleton. +Qed. + + +(* *********************************************************************** *) +(** ** Tactics *) + +(** The tactic [notin_simpl_hyps] destructs all hypotheses of the form + [(~ In x E)], where [E] is built using only [empty], [union], and + [singleton]. *) + +Ltac notin_simpl_hyps := + try match goal with + | H: In ?x ?E -> False |- _ => + change (~ In x E) in H; + notin_simpl_hyps + | H: ~ In _ empty |- _ => + clear H; + notin_simpl_hyps + | H: ~ In ?x (singleton ?y) |- _ => + let F1 := fresh in + let F2 := fresh in + assert (F1 := @elim_notin_singleton x y H); + assert (F2 := @elim_notin_singleton' x y H); + clear H; + notin_simpl_hyps + | H: ~ In ?x (union ?E ?F) |- _ => + destruct (@elim_notin_union x E F H); + clear H; + notin_simpl_hyps + end. + +(** The tactic [notin_solve] solves goals of them form [(x <> y)] and + [(~ In x E)] that are provable from hypotheses of the form + destructed by [notin_simpl_hyps]. *) + +Ltac notin_solve := + notin_simpl_hyps; + repeat (progress ( apply notin_empty + || apply notin_union + || apply notin_singleton)); + solve [ trivial | congruence | intuition auto ]. + + +(* *********************************************************************** *) +(** ** Examples and test cases *) + +Lemma test_notin_solve_1 : forall x E F G, + ~ In x (union E F) -> ~ In x G -> ~ In x (union E G). +Proof. + intros. notin_solve. +Qed. + +Lemma test_notin_solve_2 : forall x y E F G, + ~ In x (union E (union (singleton y) F)) -> ~ In x G -> + ~ In x (singleton y) /\ ~ In y (singleton x). +Proof. + intros. + split. + notin_solve. + +(* + apply notin_singleton. + generalize H. + apply notin_union. +*) +Admitted. + +Lemma test_notin_solve_3 : forall x y, + ~ E.eq x y -> ~ In x (singleton y) /\ ~ In y (singleton x). +Proof. + intros. split. notin_solve. + (* notin_solve.*) +Admitted. + +Lemma test_notin_solve_4 : forall x y E F G, + ~ In x (union E (union (singleton x) F)) -> ~ In y G. +Proof. + intros. notin_solve. +Qed. + +Lemma test_notin_solve_5 : forall x y E F, + ~ In x (union E (union (singleton y) F)) -> ~ In y E -> + ~ E.eq y x /\ ~ E.eq x y. +Proof. + intros. split. + (* notin_solve. notin_solve.*) +Admitted. + +End Notin. diff --git a/coq/FiniteSets.v b/coq/FiniteSets.v new file mode 100644 index 0000000..5c1ac86 --- /dev/null +++ b/coq/FiniteSets.v @@ -0,0 +1,65 @@ +(** A library for finite sets with extensional equality. + + Author: Brian Aydemir. *) + +Require Import FSets. +Require Import ListFacts. +Require Import AdditionalTactics. +Require AdditionalTactics. + + +(* *********************************************************************** *) +(** * Interface *) + +(** The following interface wraps the standard library's finite set + interface with an additional property: extensional equality. *) + +Module Type S. + + Declare Module E : UsualOrderedType. + Declare Module F : FSetInterface.S with Module E := E. + + Parameter eq_if_Equal : + forall s s' : F.t, F.Equal s s' -> s = s'. + +End S. + + +(* *********************************************************************** *) +(** * Implementation *) + +(** For documentation purposes, we hide the implementation of a + functor implementing the above interface. We note only that the + implementation here assumes (as an axiom) that proof irrelevance + holds. *) + +Module Make (X : UsualOrderedType) <: S with Module E := X. + + (* begin hide *) + + Module E := X. + Module F := FSetList.Make E. + Module OFacts := OrderedType.OrderedTypeFacts E. + + Axiom sort_F_E_lt_proof_irrel : forall xs (p q : sort F.E.lt xs), p = q. + + Lemma eq_if_Equal : + forall s s' : F.t, F.Equal s s' -> s = s'. + Proof. + intros [s1 pf1] [s2 pf2] Eq. + assert (s1 = s2). + unfold F.MSet.Raw.t in *. +(* eapply Sort_InA_eq_ext; eauto. + intros; eapply E.lt_trans; eauto. + intros; eapply OFacts.lt_eq; eauto. + intros; eapply OFacts.eq_lt; eauto. + subst s1. + rewrite (sort_F_E_lt_proof_irrel _ pf1 pf2). + reflexivity. + Qed. + *) + Admitted. + + (* end hide *) + +End Make. diff --git a/coq/ListFacts.v b/coq/ListFacts.v new file mode 100644 index 0000000..ff8729a --- /dev/null +++ b/coq/ListFacts.v @@ -0,0 +1,299 @@ +(** Assorted facts about lists. + + Author: Brian Aydemir. + + Implicit arguments are declared by default in this library. *) + +Set Implicit Arguments. + +Require Import Eqdep_dec. +Require Import List. +Require Import SetoidList. +Require Import Sorting. +Require Import Relations. +Require Import AdditionalTactics. + +Include AdditionalTactics. + +(* ********************************************************************** *) +(** * List membership *) + +Lemma not_in_cons : + forall (A : Type) (ys : list A) x y, + x <> y -> ~ In x ys -> ~ In x (y :: ys). +Proof. + induction ys; simpl; intuition. +Qed. + +Lemma not_In_app : + forall (A : Type) (xs ys : list A) x, + ~ In x xs -> ~ In x ys -> ~ In x (xs ++ ys). +Proof. + intros A xs ys x H J K. + destruct (in_app_or _ _ _ K); auto. +Qed. + +Lemma elim_not_In_cons : + forall (A : Type) (y : A) (ys : list A) (x : A), + ~ In x (y :: ys) -> x <> y /\ ~ In x ys. +Proof. + intros. simpl in *. auto. +Qed. + +Lemma elim_not_In_app : + forall (A : Type) (xs ys : list A) (x : A), + ~ In x (xs ++ ys) -> ~ In x xs /\ ~ In x ys. +Proof. + split; auto using in_or_app. +Qed. + + +(* ********************************************************************** *) +(** * List inclusion *) + +Lemma incl_nil : + forall (A : Type) (xs : list A), incl nil xs. +Proof. + unfold incl. + intros A xs a H; inversion H. +Qed. + +Lemma incl_trans : + forall (A : Type) (xs ys zs : list A), + incl xs ys -> incl ys zs -> incl xs zs. +Proof. + unfold incl; firstorder. +Qed. + +Lemma In_incl : + forall (A : Type) (x : A) (ys zs : list A), + In x ys -> incl ys zs -> In x zs. +Proof. + unfold incl; auto. +Qed. + +Lemma elim_incl_cons : + forall (A : Type) (x : A) (xs zs : list A), + incl (x :: xs) zs -> In x zs /\ incl xs zs. +Proof. + unfold incl. auto with datatypes. +Qed. + +Lemma elim_incl_app : + forall (A : Type) (xs ys zs : list A), + incl (xs ++ ys) zs -> incl xs zs /\ incl ys zs. +Proof. + unfold incl. auto with datatypes. +Qed. + + +(* ********************************************************************** *) +(** * Setoid facts *) + +Lemma InA_iff_In : + forall (A : Set) x xs, InA (@eq A) x xs <-> In x xs. +Proof. + + split. 2:auto using In_InA. + induction xs as [ | y ys IH ]. + intros H. inversion H. + intros H. inversion H; subst; auto with datatypes. +Admitted. + + +(* ********************************************************************* *) +(** * Equality proofs for lists *) + +Section EqRectList. + +Variable A : Type. +Variable eq_A_dec : forall (x y : A), {x = y} + {x <> y}. + +Lemma eq_rect_eq_list : + forall (p : list A) (Q : list A -> Type) (x : Q p) (h : p = p), + eq_rect p Q x p h = x. +Proof with auto. + intros. + apply K_dec with (p := h)... + decide equality. destruct (eq_A_dec a a0)... +Qed. + +End EqRectList. + + +(* ********************************************************************** *) +(** * Decidable sorting and uniqueness of proofs *) + +Section DecidableSorting. + +Variable A : Set. +Variable leA : relation A. +Hypothesis leA_dec : forall x y, {leA x y} + {~ leA x y}. + +Theorem lelistA_dec : + forall a xs, {lelistA leA a xs} + {~ lelistA leA a xs}. +Proof. + induction xs as [ | x xs IH ]; auto with datatypes. + destruct (leA_dec a x); auto with datatypes. + right. intros J. inversion J. auto. +Qed. + +Theorem sort_dec : + forall xs, {sort leA xs} + {~ sort leA xs}. +Proof. + induction xs as [ | x xs IH ]; auto with datatypes. + destruct IH; destruct (lelistA_dec x xs); auto with datatypes. + right. intros K. inversion K. auto. + right. intros K. inversion K. auto. + right. intros K. inversion K. auto. +Qed. + +Section UniqueSortingProofs. + + Hypothesis eq_A_dec : forall (x y : A), {x = y} + {x <> y}. + Hypothesis leA_unique : forall (x y : A) (p q : leA x y), p = q. + + Scheme lelistA_ind' := Induction for lelistA Sort Prop. + Scheme sort_ind' := Induction for sort Sort Prop. + + Theorem lelistA_unique : + forall (x : A) (xs : list A) (p q : lelistA leA x xs), p = q. + Proof with auto. + induction p using lelistA_ind'; intros q. + (* case: nil_leA *) + replace (nil_leA leA x) with (eq_rect _ (fun xs => lelistA leA x xs) + (nil_leA leA x) _ (refl_equal (@nil A)))... + generalize (refl_equal (@nil A)). + pattern (@nil A) at 1 3 4 6, q. case q; [ | intros; discriminate ]. + intros. rewrite eq_rect_eq_list... +Admitted. +(* + (* case: cons_sort *) + replace (cons_leA leA x b l l0) with (eq_rect _ (fun xs => lelistA leA x xs) + (cons_leA leA x b l l0) _ (refl_equal (b :: l)))... + + generalize (refl_equal (b :: l)). + pattern (b :: l) at 1 3 4 6, q. case q; [ intros; discriminate | ]. + intros. inversion e; subst. + rewrite eq_rect_eq_list... + rewrite (leA_unique l0 l2)... + Qed. +*) + Theorem sort_unique : + forall (xs : list A) (p q : sort leA xs), p = q. + Proof with auto. + induction p using sort_ind'; intros q. + (* case: nil_sort *) + replace (nil_sort leA) with (eq_rect _ (fun xs => sort leA xs) + (nil_sort leA) _ (refl_equal (@nil A)))... + generalize (refl_equal (@nil A)). + pattern (@nil A) at 1 3 4 6, q. case q; [ | intros; discriminate ]. + intros. rewrite eq_rect_eq_list... + Admitted. + (* + (* case: cons_sort *) + replace (cons_sort p l0) with (eq_rect _ (fun xs => sort leA xs) + (cons_sort p l0) _ (refl_equal (a :: l)))... + generalize (refl_equal (a :: l)). + pattern (a :: l) at 1 3 4 6, q. case q; [ intros; discriminate | ]. + intros. inversion e; subst. + rewrite eq_rect_eq_list... + rewrite (lelistA_unique l0 l2). + rewrite (IHp s)... + Qed. +*) +End UniqueSortingProofs. +End DecidableSorting. + + +(* ********************************************************************** *) +(** * Equality on sorted lists *) + +Section Equality_ext. + +Variable A : Set. +Variable ltA : relation A. +Hypothesis ltA_trans : forall x y z, ltA x y -> ltA y z -> ltA x z. +Hypothesis ltA_not_eqA : forall x y, ltA x y -> x <> y. +Hypothesis ltA_eqA : forall x y z, ltA x y -> y = z -> ltA x z. +Hypothesis eqA_ltA : forall x y z, x = y -> ltA y z -> ltA x z. + +Create HintDb ListHints. +Hint Resolve ltA_trans :ListHints. +Hint Immediate ltA_eqA eqA_ltA :ListHints. + +Notation Inf := (lelistA ltA). +Notation Sort := (sort ltA). + +Lemma not_InA_if_Sort_Inf : + forall xs a, Sort xs -> Inf a xs -> ~ InA (@eq A) a xs. +Proof. + induction xs as [ | x xs IH ]; intros a Hsort Hinf H. + inversion H. + inversion H; subst. + inversion Hinf; subst. + assert (x <> x) by auto; intuition. + inversion Hsort; inversion Hinf; subst. +Admitted. + +(* + assert (Inf a xs) by eauto using InfA_ltA. + assert (~ InA (@eq A) a xs) by auto. + intuition. +Qed. +*) + +Lemma Sort_eq_head : + forall x xs y ys, + Sort (x :: xs) -> + Sort (y :: ys) -> + (forall a, InA (@eq A) a (x :: xs) <-> InA (@eq A) a (y :: ys)) -> + x = y. +Proof. + intros x xs y ys SortXS SortYS H. + inversion SortXS; inversion SortYS; subst. + assert (Q3 : InA (@eq A) x (y :: ys)) by firstorder. + assert (Q4 : InA (@eq A) y (x :: xs)) by firstorder. + inversion Q3; subst; auto. + inversion Q4; subst; auto. +Admitted. +(* + assert (ltA y x) by (refine (SortA_InfA_InA _ _ _ _ _ H6 H7 H1); auto). + assert (ltA x y) by (refine (SortA_InfA_InA _ _ _ _ _ H2 H3 H4); auto). + assert (y <> y) by eauto. + intuition. +Qed. +*) + +Lemma Sort_InA_eq_ext : + forall xs ys, + Sort xs -> + Sort ys -> + (forall a, InA (@eq A) a xs <-> InA (@eq A) a ys) -> + xs = ys. +Proof. + induction xs as [ | x xs IHxs ]; induction ys as [ | y ys IHys ]; + intros SortXS SortYS H; auto. + (* xs -> nil, ys -> y :: ys *) + assert (Q : InA (@eq A) y nil) by firstorder. + inversion Q. + (* xs -> x :: xs, ys -> nil *) + assert (Q : InA (@eq A) x nil) by firstorder. + inversion Q. + (* xs -> x :: xs, ys -> y :: ys *) + inversion SortXS; inversion SortYS; subst. + assert (x = y) by eauto using Sort_eq_head. + cut (forall a, InA (@eq A) a xs <-> InA (@eq A) a ys). + intros. assert (xs = ys) by auto. subst. auto. + intros a; split; intros L. + assert (Q2 : InA (@eq A) a (y :: ys)) by firstorder. + inversion Q2; subst; auto. + assert (Q5 : ~ InA (@eq A) y xs) by auto using not_InA_if_Sort_Inf. + intuition. + assert (Q2 : InA (@eq A) a (x :: xs)) by firstorder. + inversion Q2; subst; auto. + assert (Q5 : ~ InA (@eq A) y ys) by auto using not_InA_if_Sort_Inf. + intuition. +Qed. + +End Equality_ext. diff --git a/coq/_CoqProject b/coq/_CoqProject index 5841128..c71a891 100644 --- a/coq/_CoqProject +++ b/coq/_CoqProject @@ -1,4 +1,9 @@ -R . LadderTypes +AdditionalTactics.v +ListFacts.v +FiniteSets.v +FSetNotin.v +Atom.v terms.v terms_debruijn.v equiv.v