Library LocConfTac

Here we effectively define the tactics that will be used to solve a critical pair.

Two mains tactics are defined for proving |- exists u, Rstar R s u /\ Rstar R t u.

try_smart_solve



The assumptions are the following:

  • The relation R is defined inductively.
  • Given a "reasonnable" open term x, any sequence of reductions eventually stops (modulo AC). If it is not the case, the tactic may loop forever.
  • Given a critical pair R r s and R r t, we can blindly reduce s and t and find AC-equivalent elements. Again, if it is not the case, the tactic could just not solve the pair.
The tactic try_smart_solve takes 3 tactics as inputs.

  • core_step. Try to prove automatically Rstar R a b for "trivial" cases. A trivial property is one that is immediate from the inductive definition of R or one that comes almost directly using congruence. In general, congruence cannot be checked by auto, this is why we need a special crafted tactic for it.
  • find_ACequiv. Takes a term x as input and produce a list of terms that are AC-equivalent to it. It is up to the user to make sure that if y is any term in the list, Rstar R x y can be proven by core_step.
  • find_nonAC. Similar, but for non-AC steps. Morally, given x tactic should catch all the non-AC terms y such that Rstar R x y can be proven by core_step.
Together with these three tactics, the tactic try_smart_solve blindly reduce from r and from s and try to show that the resulting elements are AC-equivalent. This gives u: we are done !

The tactic also takes two numerical arguments:
  • d1 is the number of AC-equivalent moves done while searching for a non-AC rewrite;
  • d2 is the number of AC-equivalent moves allowed for trying to show that the two resulting elements are AC-equivalent.

go_as_far_as_possible R core_step find_nonAC find_ACequiv



Similar as the previous one, this tactic does not try to close the pair. It just goes as far as possible alone, then pass the result on to the user to conclude.

solve_critical R core_step S L1 L2



If for some reason the tactic above cannot reach an agreement, but the user knows what is u and how to get there, it is possible to use solve_critical. Again one needs the tactic core_step, but that is all: S is the known closing element, L1 is the path to go from s to S and L2 the path to go from t to S.

To be able to use the tactic type of in ssreflect
Ltac typeof A := let x := (type of A) in constr : x.

Libraries
Require Import ssreflect.
Require Export RW.
Require Export ListTac.

Automatic solving tactic


Tool : LtacTreeRW. Each path in the tree is supposed to represent a sequence of rewrites.

Inductive LtacTreeRW (term:Set) : Prop :=
  | LtacNodeRW : term -> (list (LtacTreeRW term)) -> (LtacTreeRW term).

Implicit Arguments LtacTreeRW [term].
Implicit Arguments LtacNodeRW [term].

a map function for LtacTreeRW and list LtacTreeRW
Ltac maptree f t :=
    match t with
      | LtacNodeRW ?a ?l =>
        let aa := (f a) in
        let x := maplisttree f l in
          constr : (LtacNodeRW aa x)
    end
  with maplisttree f l :=
    match l with
      | (nil (A:=?B)) => constr : (nil (A:=B))
      | (?h :: ?t) =>
        let x := (maptree f h) in
        let y := (maplisttree f t) in
        constr : (x::y)
    end.

Retrieve all the elements of some LtacTreeRW and put them in a regular list
Ltac list_of_LtacTreeRW x :=
  match x with
    | LtacNodeRW ?a ?l =>
      let U := typeof a in
      let x := list_of_LtacTreeRW_list U l in
        constr : (a::x)
  end
with list_of_LtacTreeRW_list U l :=
  match l with
    | nil => constr : (nil (A:=U))
    | ?h::?t =>
      let x := list_of_LtacTreeRW h in
        let y := list_of_LtacTreeRW_list U t in
          let z := applist x y in
            constr : z
  end.

Take as input H : Rstar R a x, a list y::...::z::nil and x and makes H into H : Rstar R a z recursively using a provided tactic core_step.

Ltac solve_list_R R core_step H l x:=
  match l with
    | nil => idtac
    | ?a :: ?b =>
      let A := fresh in
      (have A : (Rstar R x a));
      [ by core_step |
        (have := (Rstar_trans _ _ _ _ H A) => {A H} H);
        solve_list_R R core_step H b a]
  end.

Given a sequence of paths as a tree, extend the paths one step further using find_ACequiv. Do not add the elements that appear in the list known
Ltac iter_ACequiv find_ACequiv known t :=
    match t with
      | LtacNodeRW ?h nil =>
        let x := find_ACequiv h in
        let B := typeof t in
        let x':= remlistinlist known x in
        let f := (fun z => constr : (LtacNodeRW z nil)) in
        let y := maplist f B x' in
          constr : (LtacNodeRW h y)
      | LtacNodeRW ?h ?t =>
        let x := iter_AC_equiv_list find_ACequiv known t in
          constr : (LtacNodeRW h x)
    end
  with iter_AC_equiv_list find_ACequiv known l :=
    match l with
      | (?h :: ?t) =>
        let x := iter_ACequiv find_ACequiv known h in
        let y := iter_AC_equiv_list find_ACequiv known t in
          constr : (x :: y)
      | ?a => constr : a
    end.

Produce a tree of depth depth of AC-equivalent things starting from some term r. Again, we use the provided tactic find_ACequiv

Ltac get_ACequiv find_ACequiv depth r :=
    match depth with
      | 0 =>
        let t := (find_ACequiv r) in
        let B := typeof r in
        let f := (fun z => constr : (LtacNodeRW z nil)) in
        let y := maplist f (LtacTreeRW (term:=B)) t in
          constr : (LtacNodeRW r y)
      | S ?m =>
        let x := get_ACequiv find_ACequiv m r in
        let known := list_of_LtacTreeRW x in
          iter_ACequiv find_ACequiv known x
    end.

Try to produce an hypothesis H : Rstar R a b using AC-equivalence:
  • Assert H : Rstar R a b.
  • To prove it does indeed hold, assert K : Rstar R a a.
  • Construct the AC-tree from a.
  • Read the paths a..c stored in the tree: for each of them, extend K to K : Rstar R a c and see if it is enough to conclude.
Ltac show_ACequiv R core_step find_ACequiv depth H a b :=
  have H : (Rstar R a b); first (
    let K := fresh in have K : (Rstar R a a); first auto;
  let rec test_from_list p l :=
    match l with
      | nil => fail
      | ?h :: ?t =>
        first [
            test_from_tree p h
          | test_from_list p t
        ]
    end
  with test_from_tree p t :=
    match t with
      | LtacNodeRW ?b ?l =>
        let q := constr : (b::nil) in
        let path := applist p q in
        first [
            match path with
              | (?h :: ?q) => idtac path; by solve_list_R R core_step K q a
              | nil => fail
            end
          | test_from_list path l
        ]
    end
  in let t := (get_ACequiv find_ACequiv depth a) in
    match (typeof a) with
      | ?term => idtac t; try test_from_tree (nil (A:=term)) t
    end).

Prove a goal of the form Rstar R a b where a and b are AC-equivalent.
Ltac try_ACequiv R core_step find_ACequiv depth :=
  match goal with
    | [ |- Rstar R ?a ?b ] =>
      let H := fresh in
        show_ACequiv R core_step find_ACequiv depth H a b; auto
    | _ => idtac "fail: try deeper?"
  end.

Tool: LtacMaybe is a maybe monad for terms
Inductive LtacMaybe (term:Set) : Prop :=
| LtacYes : term -> LtacMaybe term
| LtacNo : LtacMaybe term.

Implicit Arguments LtacMaybe [term].
Implicit Arguments LtacYes [term].
Implicit Arguments LtacNo [term].

Does the same thing as search_next, but modulo AC, using AC-rewrite of length at most depth. The auxiliary functions search_next_from_list and search_next_from_tree look for an element in the tree starting from x that would rewrite to some y in a non-AC way and output the path from x to y as a list of terms.

Ltac search_next_modAC find_nonAC find_ACequiv depth x :=
  let U := typeof x in
  let rec search_next_from_list l :=
    match l with
      | nil => constr : (nil (A:=U))
      | ?h :: ?t =>
        let x := search_next_from_tree h in
          match x with
            | nil =>
              let y := search_next_from_list t in
                constr : y
            | _ => constr : x
          end
    end
  with search_next_from_tree t :=
    match t with
      | LtacNodeRW ?a ?l =>
        let a' := find_nonAC a in
        match a' with
          | LtacNo =>
            let x := search_next_from_list l in
              match x with
                | nil => constr : (nil (A:=U))
                | _ => constr : (a::x)
              end
          | LtacYes ?b => constr : (a::b::nil)
        end
    end
  in let d := (get_ACequiv find_ACequiv depth x) in
    search_next_from_tree d.

To remove hypotheses of the form Rstar R a a.
Ltac remove_refl :=
  match goal with
    | [ H : Rstar _ ?a ?a |- _ ] => clear H; remove_refl
    | _ => idtac
  end.

Take H : Rstar R a b and turn it to H : Rstar R a c where Rstar R b c is a non-AC-equiv thing.

Ltac exhaust_Rstar R core_step find_nonAC find_ACequiv depth H :=
  move : H;
      match goal with
        | [ |- Rstar R ?a ?b -> _ ] =>
          let c := (search_next_modAC find_nonAC find_ACequiv depth b) in
            move => H;
            idtac b;
            idtac c;
            match c with
              | nil => idtac
              | _::?l => solve_list_R R core_step H l b
            end
      end.

Now, the proof of exists u, Rstar R r u /\ Rstar R s u goes as follows:
  • assert Rstar R r r and Rstar R s s
  • use exhaust_Rstar to get r' and s'
  • set u to be s'
  • show Rstar R r' s' using try_ACequiv

Ltac try_smart_solve R core_step find_nonAC find_ACequiv d1 d2 :=
  let H := fresh in let K := fresh in let L := fresh in
    match goal with
      | [ |- (exists u:_, Rstar R ?r _ /\ Rstar R ?s _)] => idtac "yes";
        (have H : (Rstar R r r)); first (by apply Rzero);
          (have K : (Rstar R s s)); first (by apply Rzero)
    end;
    move : H; (repeat progress (exhaust_Rstar R core_step find_nonAC find_ACequiv d1 K)); move => H;
    move : K; (repeat progress (exhaust_Rstar R core_step find_nonAC find_ACequiv d1 H)); move => K;
    move : H K;
    match goal with
      | [ |- Rstar R _ ?r' -> Rstar R _ ?s' -> _ ] => idtac r'; idtac s';
        move => H K;
          (have L : (Rstar R r' s')); first (clear H K; by try_ACequiv R core_step find_ACequiv d2);
            exists s'
    end;
    split; [apply (Rstar_trans _ _ _ _ H L) | auto].

The tactic that tries to go as far asa possible by itself



It simply uses exhaust_Rstar as much as possible on both side of the critical pair.


Ltac go_as_far_as_possible R core_step find_nonAC find_ACequiv :=
  let H := fresh in let K := fresh in let L := fresh in
  let L1:= fresh in let L2:= fresh in let u' := fresh in
  match goal with
    | [ |- (exists u:_, Rstar R ?r _ /\ Rstar R ?s _)] => idtac "yes";
      (have H : (Rstar R r r)); first (by apply Rzero);
        (have K : (Rstar R s s)); first (by apply Rzero)
  end;
  move : H; (repeat progress (exhaust_Rstar R core_step find_nonAC find_ACequiv 3 K)); move => H;
  move : K; (repeat progress (exhaust_Rstar R core_step find_nonAC find_ACequiv 3 H)); move => K;
  move : H K;
    match goal with
      | [ |- Rstar R _ ?r' -> Rstar R _ ?s' -> _ ] => idtac r'; idtac s';
        move => H K;
          (suff L : (exists u, Rstar R r' u /\ Rstar R s' u));
          [ (elim L => u' [L1 L2]; exists u'; split; solve_Rstar_trans) | ]
    end.

The fine-tuned tactic for solving critical pairs by hand


Ltac make_R_Rstar R :=
  match goal with
    | [ H : R ?a ?b |- _ ] =>
      (have : (Rstar R a b));
      first (by (apply R_Rstar; auto)); move => {H} H;
        make_R_Rstar R
    | _ => idtac
  end.

Special list for writing path : LRone means "we are one step from the goal, do it automagically", and LRzero says "we are already there, apply Rzero".

Inductive List_Rewrite (term:Set) : Prop :=
| LRone : List_Rewrite term
| LRzero : List_Rewrite term
| LRcons : term -> List_Rewrite term -> List_Rewrite term.

Implicit Arguments LRone [term].
Implicit Arguments LRzero [term].
Implicit Arguments LRcons [term].

Ltac solve_list_R_fine core_step l s :=
  match l with
    | LRzero => apply Rzero
    | LRone => solve_list_R_fine core_step (LRcons s LRzero) s
    | LRcons ?a ?b =>
      apply (Rstar_trans _ _ a _);
        first (core_step);
          solve_list_R_fine core_step b s
  end.

This is the tactic to use : The element closing the pair is S, the left path is L1 and the right path is L2. Note that the path does not contain the known element we start from.

Ltac solve_critical R core_step S L1 L2 :=
  make_R_Rstar R;
  exists S; split; [solve_list_R_fine core_step L1 S | solve_list_R_fine core_step L2 S].

Notation for this super-duper list

Infix ":::" := LRcons (at level 60, right associativity).