Verus automatically selects non-user-selectable triggers

[matthias-brun]

Verus disallows user-chosen triggers on tuple constructors (e.g. #[trigger] (a, b)) but automatically selected triggers sometimes do involve tuples. E.g. the following example has no valid user-selectable triggers but Verus automatically picks a trigger involving the tuple constructor.

use vstd::prelude::*; verus!{

struct Foo { s: (usize,usize) }

proof fn f()
    ensures forall|f: Foo, a: usize, b: usize| f.s == (a, b) ==> true
{}

}

This generates the following AIR for the ensures:

;; Function-Specs test::f
(declare-fun ens%test!f. (Int) Bool)
(axiom (forall ((no%param Int)) (!
   (= (ens%test!f. no%param) (forall ((f$ Poly) (a$ Poly) (b$ Poly)) (!
      true
      :pattern ((test!Foo./Foo/s (%Poly%test!Foo. f$)) (tuple%2./tuple%2 a$ b$))
      :qid user_test__f_0
      :skolemid skolem_user_test__f_0
   )))
   :pattern ((ens%test!f. no%param))
   :qid internal_ens__test!f._definition
   :skolemid skolem_internal_ens__test!f._definition
)))

I vaguely remember there being a discussion about triggering on tuples being important for some particular use case (maybe at the Verus retreat?) so I'm wondering if this is intentional or not. It is certainly surprising behavior.

[utaal]

Relevant: #1199