33. Voluntary change under the rule in force🔗

Requirement ONE-504. Of its 4 acceptance criteria, 4 are proven.

rule

Rules.OneOrder.Offers.voluntaryChange
  (e : Rules.OneOrder.Offers.ExpiryReading)
  (rules : List Rules.OneOrder.Offers.Restriction)
  (j : Rules.OneOrder.Offers.Journey)
  (req : Rules.OneOrder.Offers.ChangeRequest) :
  Rules.OneOrder.Offers.ChangeDecision
Rules.OneOrder.Offers.voluntaryChange
  (e :
    Rules.OneOrder.Offers.ExpiryReading)
  (rules :
    List
      Rules.OneOrder.Offers.Restriction)
  (j : Rules.OneOrder.Offers.Journey)
  (req :
    Rules.OneOrder.Offers.ChangeRequest) :
  Rules.OneOrder.Offers.ChangeDecision

EARS: When a customer asks for a voluntary change, the system shall refuse it if the rule in force forbids it, and otherwise quote it with the rule's fee as the penalty.

Story: As a customer, I want a change to cost what the rule in force says, so that I pay the fee and the fare difference and nothing else.

Acceptance criteria:

ONE-504.1: If the rule in force forbids a change of the kind asked for, then the system shall refuse the change.
ONE-504.2: When the rule in force allows a change and states a fee, the system shall quote the change with that fee as its penalty.
ONE-504.3: When the rule in force allows a change and states no fee, the system shall quote the change with no penalty.
ONE-504.4: When the rule in force allows a change with a fee no larger than the price of the items changed, and the seller does not ask to keep the value for later use, the system shall price the change so that the customer owes the fee plus the fare difference, net of what the airline returns.

The quote is a change for ONE-201 to price (Change.priceDifferential): the old and new prices, the fee as the penalty, and nothing forfeited. When no rule is in force the decision says so; the guide does not say what applies then.

33.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-504.1	Proven	Change decisions, Forbidden changes are refused
ONE-504.2	Proven	Change decisions, Rule's fee is the penalty
ONE-504.3	Proven	Change decisions, No fee, no penalty
ONE-504.4	Proven	Change decisions, Voluntary change under a restriction

33.2. Guarantees🔗

33.2.1. Forbidden changes are refused🔗

guarantee

Rules.OneOrder.Offers.change_refused
  (e : Rules.OneOrder.Offers.ExpiryReading)
  (rules : List Rules.OneOrder.Offers.Restriction)
  (j : Rules.OneOrder.Offers.Journey)
  (req : Rules.OneOrder.Offers.ChangeRequest)
  (r : Rules.OneOrder.Offers.Restriction)
  (h :
    Rules.OneOrder.Offers.ruleInForce e rules j
        (Rules.OneOrder.Offers.Action.change req.kind) req.requestedAt =
      some r)
  (hr : r.allowed = false) :
  Rules.OneOrder.Offers.voluntaryChange e rules j req =
    Rules.OneOrder.Offers.ChangeDecision.refused
Rules.OneOrder.Offers.change_refused
  (e :
    Rules.OneOrder.Offers.ExpiryReading)
  (rules :
    List
      Rules.OneOrder.Offers.Restriction)
  (j : Rules.OneOrder.Offers.Journey)
  (req :
    Rules.OneOrder.Offers.ChangeRequest)
  (r : Rules.OneOrder.Offers.Restriction)
  (h :
    Rules.OneOrder.Offers.ruleInForce e
        rules j
        (Rules.OneOrder.Offers.Action.change
          req.kind)
        req.requestedAt =
      some r)
  (hr : r.allowed = false) :
  Rules.OneOrder.Offers.voluntaryChange e
      rules j req =
    Rules.OneOrder.Offers.ChangeDecision.refused

A change the rule in force forbids is refused.

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

Checks acceptance criteria ONE-504.1.

33.2.2. Rule's fee is the penalty🔗

guarantee

Rules.OneOrder.Offers.change_fee_is_penalty
  (e : Rules.OneOrder.Offers.ExpiryReading)
  (rules : List Rules.OneOrder.Offers.Restriction)
  (j : Rules.OneOrder.Offers.Journey)
  (req : Rules.OneOrder.Offers.ChangeRequest)
  (r : Rules.OneOrder.Offers.Restriction)
  (h :
    Rules.OneOrder.Offers.ruleInForce e rules j
        (Rules.OneOrder.Offers.Action.change req.kind) req.requestedAt =
      some r)
  (hr : r.allowed = true) (f : Rules.Core.Money) (hf : r.fee = some f) :
  ∃ q ap,
    Rules.OneOrder.Offers.voluntaryChange e rules j req =
        Rules.OneOrder.Offers.ChangeDecision.allowed q ap ∧
      q.penalty = f
Rules.OneOrder.Offers.change_fee_is_penalty
  (e :
    Rules.OneOrder.Offers.ExpiryReading)
  (rules :
    List
      Rules.OneOrder.Offers.Restriction)
  (j : Rules.OneOrder.Offers.Journey)
  (req :
    Rules.OneOrder.Offers.ChangeRequest)
  (r : Rules.OneOrder.Offers.Restriction)
  (h :
    Rules.OneOrder.Offers.ruleInForce e
        rules j
        (Rules.OneOrder.Offers.Action.change
          req.kind)
        req.requestedAt =
      some r)
  (hr : r.allowed = true)
  (f : Rules.Core.Money)
  (hf : r.fee = some f) :
  ∃ q ap,
    Rules.OneOrder.Offers.voluntaryChange
          e rules j req =
        Rules.OneOrder.Offers.ChangeDecision.allowed
          q ap ∧
      q.penalty = f

A change the rule in force allows with a fee is quoted with that fee as its penalty.

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

Checks acceptance criteria ONE-504.2.

33.2.3. No fee, no penalty🔗

guarantee

Rules.OneOrder.Offers.change_no_fee
  (e : Rules.OneOrder.Offers.ExpiryReading)
  (rules : List Rules.OneOrder.Offers.Restriction)
  (j : Rules.OneOrder.Offers.Journey)
  (req : Rules.OneOrder.Offers.ChangeRequest)
  (r : Rules.OneOrder.Offers.Restriction)
  (h :
    Rules.OneOrder.Offers.ruleInForce e rules j
        (Rules.OneOrder.Offers.Action.change req.kind) req.requestedAt =
      some r)
  (hr : r.allowed = true) (hf : r.fee = none) :
  ∃ q ap,
    Rules.OneOrder.Offers.voluntaryChange e rules j req =
        Rules.OneOrder.Offers.ChangeDecision.allowed q ap ∧
      q.penalty.amount = 0
Rules.OneOrder.Offers.change_no_fee
  (e :
    Rules.OneOrder.Offers.ExpiryReading)
  (rules :
    List
      Rules.OneOrder.Offers.Restriction)
  (j : Rules.OneOrder.Offers.Journey)
  (req :
    Rules.OneOrder.Offers.ChangeRequest)
  (r : Rules.OneOrder.Offers.Restriction)
  (h :
    Rules.OneOrder.Offers.ruleInForce e
        rules j
        (Rules.OneOrder.Offers.Action.change
          req.kind)
        req.requestedAt =
      some r)
  (hr : r.allowed = true)
  (hf : r.fee = none) :
  ∃ q ap,
    Rules.OneOrder.Offers.voluntaryChange
          e rules j req =
        Rules.OneOrder.Offers.ChangeDecision.allowed
          q ap ∧
      q.penalty.amount = 0

A change the rule in force allows without a fee is quoted with no penalty.

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

Checks acceptance criteria ONE-504.3.

33.2.4. Voluntary change under a restriction🔗

guarantee

Rules.OneOrder.Offers.change_net_is_fee_plus_difference
  (e : Rules.OneOrder.Offers.ExpiryReading)
  (rules : List Rules.OneOrder.Offers.Restriction)
  (j : Rules.OneOrder.Offers.Journey)
  (req : Rules.OneOrder.Offers.ChangeRequest)
  (q : Rules.OneOrder.Change.ChangeQuote) (ap : Bool)
  (h :
    Rules.OneOrder.Offers.voluntaryChange e rules j req =
      Rules.OneOrder.Offers.ChangeDecision.allowed q ap)
  (hfee : q.penalty.amount ≤ req.oldPrice.amount)
  (hs : req.settlement ≠ Rules.OneOrder.Change.Settlement.respend)
  (x : Rules.OneOrder.Change.ExcessPenalty)
  (d : Rules.OneOrder.Change.PriceDifferential)
  (hd : Rules.OneOrder.Change.priceDifferential x q = Except.ok d) :
  ↑d.dueToAirline.amount - ↑d.dueByAirline.amount =
    ↑req.newPrice.amount - ↑req.oldPrice.amount + ↑q.penalty.amount
Rules.OneOrder.Offers.change_net_is_fee_plus_difference
  (e :
    Rules.OneOrder.Offers.ExpiryReading)
  (rules :
    List
      Rules.OneOrder.Offers.Restriction)
  (j : Rules.OneOrder.Offers.Journey)
  (req :
    Rules.OneOrder.Offers.ChangeRequest)
  (q : Rules.OneOrder.Change.ChangeQuote)
  (ap : Bool)
  (h :
    Rules.OneOrder.Offers.voluntaryChange
        e rules j req =
      Rules.OneOrder.Offers.ChangeDecision.allowed
        q ap)
  (hfee :
    q.penalty.amount ≤
      req.oldPrice.amount)
  (hs :
    req.settlement ≠
      Rules.OneOrder.Change.Settlement.respend)
  (x :
    Rules.OneOrder.Change.ExcessPenalty)
  (d :
    Rules.OneOrder.Change.PriceDifferential)
  (hd :
    Rules.OneOrder.Change.priceDifferential
        x q =
      Except.ok d) :
  ↑d.dueToAirline.amount -
      ↑d.dueByAirline.amount =
    ↑req.newPrice.amount -
        ↑req.oldPrice.amount +
      ↑q.penalty.amount

A change the rule in force allows, with a fee no larger than the price of the items changed and no request to keep the value for later use, is priced so that the customer owes the fee plus the fare difference, net of what the airline returns. This holds under both readings of what happens to a penalty above the refundable value, and whether the fee is netted or charged separately.

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

Checks acceptance criteria ONE-504.4.

33.3. Examples🔗

33.3.1. Change decisions🔗

example

Rules.OneOrder.Offers.changeDecisions :
  List Rules.OneOrder.Offers.ChangeRow
Rules.OneOrder.Offers.changeDecisions :
  List Rules.OneOrder.Offers.ChangeRow

Given the journey and its change rules, and a trip at 500.00 EUR.

When the customer asks on 10 January for a flight change to a trip at 550.00 EUR, on 24 January at noon for the same change, and on 10 January for a name change. A customer who did not show up for the flight then asks for a name change on 2 February.

Then the first change is allowed with the 30.00 EUR fee as its penalty, and the customer pays 80.00 EUR: the fee plus the fare difference of 50.00 EUR. The second is refused. The name change is allowed with no penalty and costs nothing. At the no show no rule covers a name change, so the rules give no answer.

What Lean computed:

Request	Verdict	Penalty	Due to airline	Due by airline
flight change on 10 January	allowed	30.00 EUR	80.00 EUR	0.00 EUR
flight change on 24 January	refused	none	none	none
name change on 10 January	allowed	0.00 EUR	0.00 EUR	0.00 EUR
name change after a no show	no rule	none	none	none

Checks acceptance criteria ONE-504.1, ONE-504.2, ONE-504.3, ONE-504.4.