24. Selecting items from an offer🔗

Requirement ONE-401. Of its 4 acceptance criteria, 3 are proven and 1 is open.

rule

Rules.OneOrder.Creation.selectItems
  (o : Rules.OneOrder.Creation.MarkedOffer) (sel : List String) :
  Except Rules.OneOrder.Creation.CreateRejection
    (List Rules.OneOrder.OfferItem)
Rules.OneOrder.Creation.selectItems
  (o :
    Rules.OneOrder.Creation.MarkedOffer)
  (sel : List String) :
  Except
    Rules.OneOrder.Creation.CreateRejection
    (List Rules.OneOrder.OfferItem)

EARS: When a seller selects items from an offer, the system shall accept the selection only if it names items the offer holds and includes every item the offer marks mandatory.

Story: As a seller, I want to leave out the optional items of an offer, so that the customer pays only for what they chose.

Acceptance criteria:

ONE-401.1: If a selection names an item the offer does not hold, then the system shall reject the selection.
ONE-401.2: If a selection leaves out an item the offer marks mandatory, then the system shall reject the selection.
ONE-401.3: When a selection is accepted, the system shall take every offer item it names and no other.
ONE-401.4: When a selection is accepted, the system shall include at least one item the offer marks mandatory.

An item without the mandatory mark is optional. An empty selection is not rejected here: a request that selects nothing from any offer is rejected when the order is created (createOrder), since an order holds at least one item. The guide also asks a selection to name the passengers each item was built for; the model does not check that.

24.1. How each acceptance criterion is checked🔗

A criterion is proven when a guarantee below proves it for every input, and example only when only examples check it.

Criterion	Status	Checked by
ONE-401.1	Proven	Selecting from trip, Unknown items are rejected
ONE-401.2	Proven	Selecting from trip, Selections include the mandatory items
ONE-401.3	Proven	Selecting from trip, A selection takes the items it names
ONE-401.4	Open	Every order holds a mandatory item, Seat without flight

24.2. Guarantees🔗

24.2.1. Unknown items are rejected🔗

guarantee

Rules.OneOrder.Creation.select_rejects_unknown
  (o : Rules.OneOrder.Creation.MarkedOffer) (sel : List String)
  (id : String) (hid : id ∈ sel)
  (hnot : ∀ oi ∈ o.offer.items, oi.id ≠ id) :
  ∃ e, Rules.OneOrder.Creation.selectItems o sel = Except.error e
Rules.OneOrder.Creation.select_rejects_unknown
  (o :
    Rules.OneOrder.Creation.MarkedOffer)
  (sel : List String) (id : String)
  (hid : id ∈ sel)
  (hnot :
    ∀ oi ∈ o.offer.items, oi.id ≠ id) :
  ∃ e,
    Rules.OneOrder.Creation.selectItems o
        sel =
      Except.error e

A selection that names an item the offer does not hold is rejected.

Proven Lean checked the proof, and the proof depends on no unproven step.

Checks acceptance criteria ONE-401.1.

24.2.2. Selections include the mandatory items🔗

guarantee

Rules.OneOrder.Creation.select_rejects_missing_mandatory
  (o : Rules.OneOrder.Creation.MarkedOffer) (sel : List String)
  (id : String) (hm : id ∈ o.mandatory) (hnot : id ∉ sel) :
  ∃ e, Rules.OneOrder.Creation.selectItems o sel = Except.error e
Rules.OneOrder.Creation.select_rejects_missing_mandatory
  (o :
    Rules.OneOrder.Creation.MarkedOffer)
  (sel : List String) (id : String)
  (hm : id ∈ o.mandatory)
  (hnot : id ∉ sel) :
  ∃ e,
    Rules.OneOrder.Creation.selectItems o
        sel =
      Except.error e

A selection that leaves out an item the offer marks mandatory is rejected.

Proven Lean checked the proof, and the proof depends on no unproven step.

Checks acceptance criteria ONE-401.2.

24.2.3. A selection takes the items it names🔗

guarantee

Rules.OneOrder.Creation.select_takes_named_items
  (o : Rules.OneOrder.Creation.MarkedOffer) (sel : List String)
  (items : List Rules.OneOrder.OfferItem)
  (h : Rules.OneOrder.Creation.selectItems o sel = Except.ok items) :
  (∀ (oi : Rules.OneOrder.OfferItem),
      oi ∈ items ↔ oi ∈ o.offer.items ∧ oi.id ∈ sel) ∧
    ∀ id ∈ sel, ∃ oi ∈ items, oi.id = id
Rules.OneOrder.Creation.select_takes_named_items
  (o :
    Rules.OneOrder.Creation.MarkedOffer)
  (sel : List String)
  (items : List Rules.OneOrder.OfferItem)
  (h :
    Rules.OneOrder.Creation.selectItems o
        sel =
      Except.ok items) :
  (∀ (oi : Rules.OneOrder.OfferItem),
      oi ∈ items ↔
        oi ∈ o.offer.items ∧
          oi.id ∈ sel) ∧
    ∀ id ∈ sel, ∃ oi ∈ items, oi.id = id

An accepted selection takes exactly the offer items whose references it names, and every reference it names is an item it takes.

Proven Lean checked the proof, and the proof depends on no unproven step.

Checks acceptance criteria ONE-401.3.

24.2.4. Every order holds a mandatory item🔗

guarantee

Rules.OneOrder.Creation.select_includes_mandatory
  (o : Rules.OneOrder.Creation.MarkedOffer) (sel : List String)
  (items : List Rules.OneOrder.OfferItem)
  (h : Rules.OneOrder.Creation.selectItems o sel = Except.ok items) :
  ∃ oi ∈ items, oi.id ∈ o.mandatory
Rules.OneOrder.Creation.select_includes_mandatory
  (o :
    Rules.OneOrder.Creation.MarkedOffer)
  (sel : List String)
  (items : List Rules.OneOrder.OfferItem)
  (h :
    Rules.OneOrder.Creation.selectItems o
        sel =
      Except.ok items) :
  ∃ oi ∈ items, oi.id ∈ o.mandatory

Every accepted selection includes at least one item the offer marks mandatory.

Open question for the business. The guidance asks for at least one mandatory item in each offer and exempts a la carte offers. When an offer marks no item mandatory, every selection of its items is accepted, so a seat can be ordered without the flight it belongs to. The example seatWithoutFlight shows it. Which selections are allowed from an offer that marks no item mandatory, and may a seat or a bag be ordered without its flight?

Open The proof is not complete. See the open questions chapter.

Checks acceptance criteria ONE-401.4.

24.3. Examples🔗

24.3.1. Selecting from trip🔗

example

Rules.OneOrder.Creation.selectingFromTrip :
  List Rules.OneOrder.Creation.SelectionRow
Rules.OneOrder.Creation.selectingFromTrip :
  List
    Rules.OneOrder.Creation.SelectionRow

Given the trip offer: a flight the offer marks mandatory, and an optional bag and seat.

When a seller selects the flight and the seat, then the bag alone, then the flight and a meal the offer does not hold.

Then the flight and the seat are taken. The bag alone is rejected because the flight is missing. The meal is rejected as an item the offer does not hold.

What Lean computed:

Selected	Taken	Rejection
OI-FLT, OI-SEAT	OI-FLT, OI-SEAT	none
OI-BAG	none	missing mandatory OFF-A OI-FLT
OI-FLT, OI-MEAL	none	unknown item OFF-A OI-MEAL

Checks acceptance criteria ONE-401.1, ONE-401.2, ONE-401.3.

24.3.2. Seat without flight🔗

example

Rules.OneOrder.Creation.seatWithoutFlight :
  Except Rules.OneOrder.Creation.CreateRejection
    Rules.OneOrder.Creation.MandatoryCheck
Rules.OneOrder.Creation.seatWithoutFlight :
  Except
    Rules.OneOrder.Creation.CreateRejection
    Rules.OneOrder.Creation.MandatoryCheck

Given an a la carte offer with a flight and a seat, neither marked mandatory.

When a seller selects the seat alone.

Then the selection is accepted, and the order would hold a seat with no flight. No item the offer marks mandatory is taken, because it marks none.

What Lean computed:

Accepted. The result:

Mandatory items: none
Taken: OI-SEAT
Mandatory taken: no

Checks acceptance criteria ONE-401.4.

24.4. Open question🔗

The guarantee Every order holds a mandatory item is open: the example Seat without flight shows the rule as written breaking it. Questions from the ONE Order rules sets out the question for the team.