https://github.com/suneel-sarswat/dsam
Raw File
Tip revision: 81ed4b1c2c07db12de7e9db78fa6538ad31e01de authored by Suneel Sarswat on 23 February 2021, 12:55:22 UTC
time stamp comment added
Tip revision: 81ed4b1
SetSpecs.v




(* -----------------Description --------------------------------------------------
   
   This file summarises some useful results from List Module of standard Library. 
   We create a hint database to remember important results regarding lists (hint_list).

   Some new definitions:
   Definition Empty (s:list A):Prop := forall a : A, ~ In a s.
   Definition Equal (s s': list A) := forall a : A, In a s <-> In a s'.
   Definition Subset (s s': list A) := forall a : A, In a s -> In a s'.

   Notation "s [=] t" := (Equal s t) (at level 70, no associativity).
   Notation "s [<=] t" := (Subset s t) (at level 70, no associativity).
   Notation "| s |":= (length s) (at level 70, no associativity).

  --------------------   ------------------  ------------------------------------- *)



From Coq Require Export ssreflect  ssrbool.
Require Export Lists.List Lia.

Set Implicit Arguments.

Hint Resolve in_eq in_cons in_inv in_nil in_dec: core.

Section BasicListFacts.
  Variable A:Type.
  Lemma in_inv1 : forall (a b:A) (l:list A), In b (a :: l) -> b = a \/ In b l.
  Proof. { intros  a b l H. cut (a=b \/ In b l). 
       2: {  auto. } intros H1; destruct H1 as [H1 | H2].
       left; symmetry; auto. right;auto. } Qed.
  Lemma in_inv2: forall (x a:A) (l:list A), In x (a::l)-> x <> a -> In x l.
  Proof.  { intros x a l H. cut (x=a \/ In x l). intro H1;destruct H1 as [Hl1|Hr1].
          intro;contradiction. auto. eapply in_inv1;auto. } Qed.
  Lemma in_inv3: forall (x a:A) (l:list A), In x (a::l)-> ~ In x l -> x = a.
    Proof.  { intros x a l H. cut (x=a \/ In x l). intro H1;destruct H1 as [Hl1|Hr1].
          intro;auto. intro;contradiction.  eapply in_inv1;auto. } Qed.
  Hint Resolve in_inv1 in_inv2 in_inv3 : core.
  (*---------Some facts about NoDup on a list --------------------------------*)
  Lemma nodup_intro (a:A)(l: list A): ~ In a l -> NoDup l -> NoDup (a::l).
    Proof.  intros H1 H2; eapply NoDup_cons_iff;tauto.  Qed. 
  Lemma nodup_elim1 (a:A)(l: list A): NoDup (a::l)-> NoDup (l).
  Proof. intro H. eapply NoDup_cons_iff; eauto. Qed.
  Lemma nodup_elim2 (a:A)(l: list A): NoDup (a::l) -> ~ In a l.
    Proof. intro H. eapply NoDup_cons_iff; eauto. Qed. 
  
  Hint Immediate nodup_elim1  nodup_elim2  nodup_intro : core.
  End BasicListFacts.
Hint Resolve in_inv1 in_inv2 in_inv3: core.
Hint Immediate nodup_elim1  nodup_elim2  nodup_intro : core.



Section SetSpec.
  Variable A:Type.
  Definition Empty (s:list A):Prop := forall a : A, ~ In a s.
  
  Definition Subset (s s': list A) := forall a : A, In a s -> In a s'.
  Definition Equal (s s': list A):= Subset s s' /\ Subset s' s.
  
  (* Inductive Forall (A : Type) (P : A -> Prop) : list A -> Prop := 
     | Forall_nil : Forall P nil 
     | Forall_cons : forall (x : A) (l : list A), P x -> Forall P l -> Forall P (x :: l)  *)
  
  (* Inductive Exists (A : Type) (P : A -> Prop) : list A -> Prop :=
      |Exists_cons_hd : forall (x : A) (l : list A), P x -> Exists P (x :: l) 
      | Exists_cons_tl : forall (x : A) (l : list A), Exists P l -> Exists P (x :: l) *)
  
  (* Inductive NoDup (A : Type) : list A -> Prop := 
      | NoDup_nil : NoDup nil 
      | NoDup_cons : forall (x : A) (l : list A), ~ In x l -> NoDup l -> NoDup (x :: l) *)
End SetSpec.

Ltac unfold_spec := try(unfold Equal);try(unfold Subset);try(unfold Empty).



  Notation "s [=] t" := (Equal s t) (at level 70, no associativity).
  Notation "s [<=] t" := (Subset s t) (at level 70, no associativity).
  Notation "| s |":= (length s) (at level 70, no associativity).
  

Section BasicSetFacts.
  Variable A:Type.

  (*-----------------------Subset (spec) and its properties ------------------------*)
  Lemma Subset_intro (a:A)(l s: list A): l [<=] s -> (a::l) [<=] (a::s).
  Proof. intros H x H1.  destruct H1. subst a;auto. auto. Qed.
  Lemma Subset_intro1 (a:A)(l s: list A): l [<=] s -> l [<=] (a::s).
    Proof. intros H x H1. simpl;right;auto. Qed. 
  Lemma Subset_elim1 (a:A) (s s':list A): Subset (a:: s) s'-> In a s'.
  Proof. { unfold Subset. intro H. apply H. auto. } Qed.
   Lemma Subset_elim2 (a:A) (s s':list A): Subset (a:: s) s'->  Subset s s'.
  Proof. { unfold Subset. intro H.  intros a1 H1.
           apply H. auto. } Qed.
  Lemma self_incl (l:list A): l [<=] l.
  Proof. unfold Subset; tauto.  Qed. 
  Hint Resolve self_incl: core.

  Lemma Subset_nil (l: list A): nil [<=] l.
  Proof. unfold "[<=]"; simpl; intros; contradiction. Qed.
  Lemma Subset_of_nil (l: list A): l [<=] nil -> l=nil.
    Proof. induction l. auto. intro H. absurd (In a nil); auto. Qed.

  Lemma Subset_trans (l1 l2 l3: list A): l1 [<=] l2 -> l2 [<=] l3 -> l1 [<=] l3.
  Proof. intros H H1 x Hx1. eauto. Qed. 
 Lemma Subset_elim (a1 a2: A)(l1 l2:list A):
           (a1::l1) [<=](a2::l2) -> ~In a2 l1 ->  l1 [<=] l2.
  Proof. { unfold "[<=]". intros. assert (In a (a1 :: l1));eauto.
  apply H in H2.  destruct H2. subst a. eauto. exact. } Qed.

    Lemma Subset_elim0 (a1 a2: A)(l1 l2:list A):
           (a1::l1) [<=](a2::l2) -> ~In a2 l1 ->  a1<>a2 ->
           (a1::l1) [<=] l2.
  Proof. { unfold "[<=]". intros. apply H in H2 as H2a.  destruct H2a. subst a.
   eauto. exact. } Qed.
  Lemma Subset_elim3 (a:A)(l1 l2: list A):
       l1 [<=](a::l2) -> ~In a l1 -> l1 [<=] l2.
  Proof. unfold "[<=]". intros.  apply H in H1 as H1a.
       destruct H1a. subst. eauto. auto. Qed.
   
Hint Extern 0 (?x [<=] ?z)  =>
match goal with
| H: (x [<=] ?y) |- _ => apply (@Subset_trans  x y z)
| H: (?y [<=] z) |- _ => apply (@Subset_trans  x y z)                                   
end : core.
  
  (* ---------------------- Equal (spec) and their properties--------------------*)
  Lemma Eq_refl (s: list A):  s [=] s.
  Proof.  unfold Equal. split;auto using self_incl.  Qed. 
  Lemma Eq_sym (s s':list A): s [=] s' -> s' [=] s.
  Proof. unfold Equal.  tauto. Qed. 
  Lemma Eq_trans1 ( x y z : list A) : x [=] y -> y [=] z -> x [=] z.
  Proof. { unfold Equal.  intros H H1. destruct H as [H0 H]; destruct H1 as [H1a H1].
           split; auto.  } Qed.

 Hint Extern 0 (?x [=] ?z)  =>
match goal with
| H: (x [=] ?y) |- _ => apply (@Eq_trans1  x y z)
| H: (?y [=] z) |- _ => apply (@Eq_trans1  x y z)                                   
end : core.


  Lemma Equal_intro (s s': list A): s [<=] s' -> s' [<=] s -> s [=] s'.
  Proof. unfold "[=]".  tauto. Qed.
  Lemma Equal_intro1 (s s': list A): s = s' -> Equal s s'.
  Proof. intro; subst s; apply Eq_refl; auto. Qed.
  Lemma Equal_elim ( s s': list A): s [=] s' ->  s [<=] s' /\ s' [<=] s.
  Proof. unfold_spec; unfold iff. intros H; split; intro a;apply H. Qed.

  (* ---------------- introduction and elimination for filter operation---------- *)
  (* Check filter :  forall A : Type, (A -> bool) -> list A -> list A *)
  (* Check filter_In : forall (A : Type) (f : A -> bool) (x : A) (l : list A),
       In x (filter f l) <-> In x l /\ f x = true *)
  Lemma filter_elim1 (f: A->bool)(l: list A)(x: A): In x (filter f l)-> In x l.
  Proof. apply filter_In. Qed.
  Lemma filter_elim2 (f: A->bool)(l: list A)(x: A): In x (filter f l)-> (f x).
  Proof. apply filter_In. Qed.
  Lemma filter_intro (f: A->bool)(l: list A)(x: A): In x l -> (f x)-> In x (filter f l).
  Proof. intros; apply filter_In; split;auto. Qed.

  Hint Immediate filter_elim1 filter_elim2 filter_intro: core.


 (*--------Strong Induction, Well founded induction and set cardinality ----------*)

  
Theorem strong_induction: forall P : nat -> Prop,
                    (forall n : nat, (forall k : nat, (k < n -> P k)) -> P n) ->
                    forall n : nat, P n.
Proof. { intros P Strong_IH n.
         pose (Q:= fun (n: nat)=> forall k:nat, k<= n -> P k). 
         assert (H: Q n);unfold Q. 
         { induction n. 
           { intros k H;apply Strong_IH.
             intros k0 H1.  cut (k0 < 0). intro H2; inversion H2. lia.  } 
           { intros k H0.
             assert (H1: k < (S n) \/ k = (S n) ).  lia.
             elim H1. intro. apply IHn. lia. 
             intro H. subst k. apply Strong_IH. intros. apply IHn. lia. } }
         unfold Q in H. apply H. lia. }   Qed. 

Definition lt_set (l1 l2: list A):= |l1| < |l2|.

Lemma lt_set_is_well_founded: well_founded lt_set.
Proof. { unfold well_founded. intro a.
       remember (|a|) as n. revert Heqn. revert a.
       induction n using strong_induction.
       { intros a H1. apply Acc_intro.
         intros a0 H2. apply H with (k:= |a0|).
         subst n; apply H2. auto. } } Qed.



Lemma non_zero_size (a:A)(l: list A): In a l -> |l| > 0.
  Proof. { induction l.
         { simpl; tauto. }
         { intros. simpl. lia. } } Qed.
         
Lemma non_nil_size (l: list A): |l| > 0 -> l<>nil.
  Proof. { induction l.
         { simpl. intro H. lia. }
         { intros. intro. assert (H1: In a nil).
           rewrite <- H0. auto. destruct H1. } } Qed.
           
Lemma element_list (l: list A)(a b : A): a<>b -> In b (a::l) -> In b l.
Proof. intros H1 H2. simpl in H2. destruct H2. destruct H1;auto. exact. Qed. 

Hint Resolve non_zero_size: core.  
 
End BasicSetFacts.


   
Hint Extern 0 (?x [<=] ?z)  =>
match goal with
| H: (x [<=] ?y) |- _ => apply (@Subset_trans _ x y z)
| H: (?y [<=] z) |- _ => apply (@Subset_trans _ x y z)                                   
end : core.

Hint Extern 0 (?x [=] ?z)  =>
match goal with
| H: (x [=] ?y) |- _ => apply (@Eq_trans1 _ x y z)
| H: (?y [=] z) |- _ => apply (@Eq_trans1 _ x y z)                                   
end : core.


Hint Immediate Eq_refl Eq_sym Equal_elim Equal_intro Equal_intro1: core.
Hint Immediate  Subset_elim1 Subset_elim2 Subset_nil Subset_of_nil Subset_elim3: core.
Hint Resolve  self_incl: core.
Hint Resolve Subset_intro Subset_intro1: core.

Hint Immediate filter_elim1 filter_elim2 filter_intro: core.

Hint Resolve lt_set_is_well_founded: core.

Hint Resolve non_zero_size element_list: core. 
back to top