TC: tcalgebra/TcPolySmokeTest.ec — exercise class lemmas at parametric carrier

Add [test_addrC_at_int_poly] / [test_addrA_at_int_poly] /
[test_mulrC_at_int_poly] using [apply (addrC<:int poly>)] etc.
With the [try_delta] flush fix (commit 5e04bf6), these now work
directly — the TCIUni parked at [opentvi] gets resolved before
[tc_reducible] is checked.

[*] at carrier [int poly] still has a parser-level ambiguity
(both the section-local abbrev [Top.TcPoly.*] and the comring class
[Top.TcMonoid.*] match). Test uses [polyM] explicitly there. That
ambiguity is orthogonal to TC inference — it'd want a
disambiguation policy at the parser level.

Author: strub

examples/tcalgebra/TcPolySmokeTest.ec

@@ -79,3 +79,20 @@ qed.
 lemma test_polyLE (xs : int list) (k : int) :
   (polyL xs).[k] = nth 0 xs k.
 proof. by rewrite polyLE. qed.
+
+(* -------------------------------------------------------------------- *)
+(* Class lemmas at carrier [int poly] — exercises the parametric Path B *)
+(* path through the unifier's flush + matcher's drain.                  *)
+(* -------------------------------------------------------------------- *)
+lemma test_addrC_at_int_poly (p q : int poly) : p + q = q + p.
+proof. by apply (addrC<:int poly>). qed.
+
+lemma test_addrA_at_int_poly (p q r : int poly) :
+  p + (q + r) = (p + q) + r.
+proof. by apply (addrA<:int poly>). qed.
+
+(* [polyM] is the section-local abbrev; the comring's [( * )] is the
+   class op. With both in scope at carrier [int poly], `p * q' is
+   ambiguous at parse — use the structural lemma instead.              *)
+lemma test_mulrC_at_int_poly (p q : int poly) : polyM p q = polyM q p.
+proof. by apply polyM_mulrC. qed.