Commit 6fe27bb5 by Ralf Jung

### improve f_equiv and solve_proper; use them in a few more places

parent eb091d1d
 ... @@ -257,22 +257,28 @@ Ltac f_equiv := ... @@ -257,22 +257,28 @@ Ltac f_equiv := let H := fresh "Proper" in let H := fresh "Proper" in assert (Proper (R ==> R ==> R) f) as H by (eapply _); assert (Proper (R ==> R ==> R) f) as H by (eapply _); apply H; clear H; f_equiv apply H; clear H; f_equiv (* Next, try to infer the relation *) (* Next, try to infer the relation. Unfortunately, there is an instance of Proper for (eq ==> _), which will always be matched. *) (* TODO: Can we exclude that instance? *) (* TODO: If some of the arguments are the same, we could also (* TODO: If some of the arguments are the same, we could also query for "pointwise_relation"'s. But that leads to a combinatorial query for "pointwise_relation"'s. But that leads to a combinatorial explosion about which arguments are and which are not the same. *) explosion about which arguments are and which are not the same. *) | |- ?R (?f ?x) (?f _) => | |- ?R (?f ?x) (?f _) => let R1 := fresh "R" in let H := fresh "Proper" in let R1 := fresh "R" in let H := fresh "HProp" in let T := type of x in evar (R1: relation T); let T := type of x in evar (R1: relation T); assert (Proper (R1 ==> R) f) as H by (subst R1; eapply _); assert (Proper (R1 ==> R) f) as H by (subst R1; eapply _); subst R1; apply H; clear H; f_equiv subst R1; apply H; clear H; f_equiv | |- ?R (?f ?x ?y) (?f _ _) => | |- ?R (?f ?x ?y) (?f _ _) => let R1 := fresh "R" in let R2 := fresh "R" in let R1 := fresh "R" in let R2 := fresh "R" in let H := fresh "Proper" in let H := fresh "HProp" in let T1 := type of x in evar (R1: relation T1); let T1 := type of x in evar (R1: relation T1); let T2 := type of y in evar (R2: relation T2); let T2 := type of y in evar (R2: relation T2); assert (Proper (R1 ==> R2 ==> R) f) as H by (subst R1 R2; eapply _); assert (Proper (R1 ==> R2 ==> R) f) as H by (subst R1 R2; eapply _); subst R1 R2; apply H; clear H; f_equiv subst R1 R2; apply H; clear H; f_equiv (* In case the function symbol differs, but the arguments are the same, maybe we have a pointwise_relation in our context. *) | H : pointwise_relation _ ?R ?f ?g |- ?R (?f ?x) (?g ?x) => apply H; f_equiv end | idtac (* Let the user solve this goal *) end | idtac (* Let the user solve this goal *) ]. ]. ... @@ -289,6 +295,10 @@ Ltac solve_proper := ... @@ -289,6 +295,10 @@ Ltac solve_proper := end; end; (* Unfold the head symbol, which is the one we are proving a new property about *) (* Unfold the head symbol, which is the one we are proving a new property about *) lazymatch goal with lazymatch goal with | |- ?R (?f _ _ _ _ _ _ _ _) (?f _ _ _ _ _ _ _ _) => unfold f | |- ?R (?f _ _ _ _ _ _ _) (?f _ _ _ _ _ _ _) => unfold f | |- ?R (?f _ _ _ _ _ _) (?f _ _ _ _ _ _) => unfold f | |- ?R (?f _ _ _ _ _) (?f _ _ _ _ _) => unfold f | |- ?R (?f _ _ _ _) (?f _ _ _ _) => unfold f | |- ?R (?f _ _ _ _) (?f _ _ _ _) => unfold f | |- ?R (?f _ _ _) (?f _ _ _) => unfold f | |- ?R (?f _ _ _) (?f _ _ _) => unfold f | |- ?R (?f _ _) (?f _ _) => unfold f | |- ?R (?f _ _) (?f _ _) => unfold f ... @@ -296,6 +306,7 @@ Ltac solve_proper := ... @@ -296,6 +306,7 @@ Ltac solve_proper := end; end; solve [ f_equiv ]. solve [ f_equiv ]. (** Given a tactic [tac2] generating a list of terms, [iter tac1 tac2] (** Given a tactic [tac2] generating a list of terms, [iter tac1 tac2] runs [tac x] for each element [x] until [tac x] succeeds. If it does not runs [tac x] for each element [x] until [tac x] succeeds. If it does not suceed for any element of the generated list, the whole tactic wil fail. *) suceed for any element of the generated list, the whole tactic wil fail. *) ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!