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.
The assumptions are the following:
The tactic also takes two numerical arguments:
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.
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.
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.
- 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.
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
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.
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.
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.
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).
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.
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].
| 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.
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.
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