aac_fset_test.v

Set Warnings "-notation-overridden".
From mathcomp Require Import all_ssreflect seq.
Set Warnings "notation-overridden".

From extructures Require Import ord fset.
Open Scope fset_scope.

Set Bullet Behavior "Strict Subproofs".
Set Default Goal Selector "!".
Set Primitive Projections.


Definition T := nat_ordType.

Parameter a : T.
Parameter b : T.
Parameter c : T.

Definition fset_ab : {fset T} :=
  fset [:: a ; b].

(* We want to automate reasoning for simple fset expressions such as this one. *)
Definition Goal_subset :=
  fsubset fset_ab
          (fset0 :|: (fset_ab :|: fset [:: c])
                 :|: (fset0 :|: (fset_ab :|: fset [:: c]))).

Section ExampleProof.
  Definition manual_proof : Goal_subset.
    unfold  Goal_subset.
    rewrite !fset0U.
    apply fsubsetU.
    apply /orP. left.
    apply fsubsetU.
    apply /orP.
    left.
    apply fsubsetxx.
  Qed.

  Definition auto_proof : Goal_subset.
    unfold  Goal_subset.
    rewrite !fset0U.
    (* Moving info_eauto up one line gets very slow. *)
    info_eauto 9 using fset0U, fsubsetxx, introTF, orP, fsubsetU.
  Qed.
End ExampleProof.

Require Arith ZArith Lia.

From AAC_tactics
Require Import AAC.
From AAC_tactics
Require Instances.

Section Fset_aac.

  Instance aac_eq_equiv A : @Equivalence A eq.
  apply Build_Equivalence.
  - unfold Reflexive. auto.
  - unfold Symmetric. auto.
  - unfold Transitive. intros; subst; reflexivity.
  Qed.

  Instance aac_union_Assoc : Associative eq (@fsetU T).
  unfold Associative.
  apply fsetUA.
  Qed.

  Instance aac_union_Comm : Commutative eq (@fsetU T).
  unfold Commutative.
  apply fsetUC.
  Qed.

  Instance aac_union_proper : Proper (eq ==> eq ==> eq) (@fsetU T).
  repeat intro.
  subst.
  reflexivity.
  Qed.

  (* The aac normalisation does not cancel the unit for unions `@fset0 T`
     unless it is folded as a definition, here `O`. *)
  Definition O := @fset0 T.

  Instance aac_union_Zero A : Unit eq (@fsetU A) (@fset0 A).
  apply Build_Unit.
  - apply fset0U.
  - apply fsetU0.
  Qed.

  Instance aac_union_O : Unit eq (@fsetU T) O.
  unfold O. apply aac_union_Zero.
  Qed.

  Instance aac_union_Idem : Idempotent eq (@fsetU T).
  unfold Idempotent.
  apply fsetUid.
  Qed.

  Definition goal_union :=
    (fset0 :|: (fset_ab :|: fset [:: c])
           :|: (fset0 :|: (fset_ab :|: fset [:: c])))
    =
      ((fset0 :|: (fset_ab :|: fset [:: c]))
         :|:
         fset0 :|: (fset_ab :|: fset [:: c])).
  Goal goal_union.
    unfold goal_union.
    fold O.
    aac_normalise.
    reflexivity.
  Qed.

  (* An unsuccessful attempt to make aac_normalise work in the subset goal below. *)
  Context {H : Proper ((@fsubset T) ==> (@fsubset T) ==> (@fsubset T)) (@fsetU T)}.
  Instance X : Proper ((@fsubset T) ==> (@fsubset T) ==> (@fsubset T)) (@fsetU T) := H.

  Goal Goal_subset.
    unfold Goal_subset.
    fold O.
    (* Here we'd like to normalise, but `aac_normalise` fails with
       "Error: [aac_tactics] The goal is not an applied relation" *)
    (* aac_normalise. *)

    (* Manually pull out the equation we expect *)
    replace     (O :|: (fset_ab :|: fset [:: c])
     :|: (O :|: (fset_ab :|: fset [:: c]))) with
      (fset_ab :|: fset [::c]).
    2: aac_reflexivity.
    info_eauto using introTF, orP, fsubsetxx, fsubsetU.
  Qed.
  (* Qed fails with the error message

^
Error: Illegal application:
The term "@lift_reflexivity" of type
 "forall (X : Type) (R E : Relation_Definitions.relation X),
  AAC_lift R E -> Reflexive R -> forall x y : X, E x y -> R x y"
cannot be applied to the terms
 "{fset T}" : "Type"
 "eq" : "{fset T} -> {fset T} -> Prop"
 "eq" : "{fset T} -> {fset T} -> Prop"
 "aac_lift_subrelation" : "AAC_lift eq eq"
 "eq_Reflexive" : "Reflexive eq"
 "fset_ab :|: fset [:: c]" : "{fset T}"
 "O :|: (fset_ab :|: fset [:: c]) :|: (O :|: (fset_ab :|: fset [:: c]))"
   : "{fset T}"
 "let env_sym :=
    sigma_get
      {|
        Internal.Sym.ar := 0;
        Internal.Sym.value := fset [:: c];
        Internal.Sym.morph :=
          Reflexive_partial_app_morphism (reflexive_proper fset)
            (eq_proper_proxy [:: c])
      |}
      (sigma_add 1%AC
         {|
           Internal.Sym.ar := 0;
           Internal.Sym.value := fset_ab;
           Internal.Sym.morph := proper_eq fset_ab
         |} (sigma_empty Internal.Sym.pack)) in
  let env_bin :=
    sigma_get
      {|
        Internal.Bin.value := fsetU;
        Internal.Bin.compat := aac_union_proper;
        Internal.Bin.assoc := aac_union_Assoc;
        Internal.Bin.comm := Some aac_union_Comm;
        Internal.Bin.idem := Some aac_union_Idem
      |} (sigma_empty Internal.Bin.pack) in
  let env_units :=
    sigma_get
      {|
        Internal.u_value := O;
        Internal.u_desc :=
          [:: {| Internal.uf_idx := 1%AC; Internal.uf_desc := aac_union_O |}]
      |} (sigma_empty (Internal.unit_pack env_bin)) in
  let tty := Internal.T env_sym in
  let rsum := Internal.sum (e_sym:=env_sym) in
  let rprd := Internal.prd (e_sym:=env_sym) in
  let rsym := Internal.sym (e_sym:=env_sym) in
  let vnil := Internal.vnil env_sym in
  let vcons := Internal.vcons (e_sym:=env_sym) in
  let eval := Internal.eval (e_sym:=env_sym) env_units in
  let left :=
    rsum 1%AC
      (Utils.cons (rsym 1%AC vnil, 1%AC)
         (Utils.nil (rsym (BinNums.xO 1%AC) vnil, 1%AC))) in
  let right :=
    rsum 1%AC
      (Utils.cons
         (rsum 1%AC
            (Utils.cons (Internal.unit env_sym (BinNums.xO 1%AC), 1%AC)
               (Utils.nil
                  (rsum 1%AC
                     (Utils.cons (rsym 1%AC vnil, 1%AC)
                        (Utils.nil (rsym (BinNums.xO 1%AC) vnil, 1%AC))),
                  1%AC))), 1%AC)
         (Utils.nil
            (rsum 1%AC
               (Utils.cons (Internal.unit env_sym (BinNums.xO 1%AC), 1%AC)
                  (Utils.nil
                     (rsum 1%AC
                        (Utils.cons (rsym 1%AC vnil, 1%AC)
                           (Utils.nil (rsym (BinNums.xO 1%AC) vnil, 1%AC))),
                     1%AC))), 1%AC))) in
  Internal.decide env_units left right (erefl Eq)
  <:
  fset_ab :|: fset [:: c] =
  O :|: (fset_ab :|: fset [:: c]) :|: (O :|: (fset_ab :|: fset [:: c]))"
   : "fset_ab :|: fset [:: c] =
      O :|: (fset_ab :|: fset [:: c]) :|: (O :|: (fset_ab :|: fset [:: c]))"
The 1st term has type "Type@{max(Set,Ord.type.u0)}"
which should be coercible to "Type@{AAC_tactics.AAC.271}".
 *)


End Fset_aac.