34. Refund owed on voluntary cancellation🔗

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

rule

Rules.OneOrder.Offers.cancellationRefund
  (e : Rules.OneOrder.Offers.ExpiryReading)
  (ff : Rules.OneOrder.Offers.FullOrFixed)
  (rules : List Rules.OneOrder.Offers.Restriction)
  (j : Rules.OneOrder.Offers.Journey) (now : Rules.Core.Instant)
  (item : Rules.OneOrder.Offers.CancelledItem) :
  Rules.OneOrder.Offers.RefundDecision
Rules.OneOrder.Offers.cancellationRefund
  (e :
    Rules.OneOrder.Offers.ExpiryReading)
  (ff : Rules.OneOrder.Offers.FullOrFixed)
  (rules :
    List
      Rules.OneOrder.Offers.Restriction)
  (j : Rules.OneOrder.Offers.Journey)
  (now : Rules.Core.Instant)
  (item :
    Rules.OneOrder.Offers.CancelledItem) :
  Rules.OneOrder.Offers.RefundDecision

EARS: When a customer cancels an unused order item voluntarily, the system shall return what the cancel rule in force gives: nothing if it forbids cancellation, and otherwise a full or a fixed refund.

Story: As a customer, I want a cancellation to return what the rule in force promised, so that I know what I get back before I cancel.

Acceptance criteria:

ONE-505.1: If the cancel rule in force forbids cancellation, then the system shall return nothing.
ONE-505.2: When the cancel rule in force allows cancellation with a full refund and no fixed amount, the system shall return the item's whole price.
ONE-505.3: When the cancel rule in force allows cancellation with a fixed refund not marked full, the system shall return that amount.
ONE-505.4: When the cancel rule in force allows cancellation and sends the refund to the original form of payment, the system shall pay the refund to the original form of payment.
ONE-505.5: When an unused item is cancelled voluntarily, the system shall return at least the taxes, fees and charges in its price that are flagged refundable.

Which amount a refund marked full and also given a fixed amount returns is a reading of the guide (FullOrFixed). When no cancel rule is in force the decision says so; the guide does not say what applies then.

34.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-505.1	Proven	Forbidden cancellation returns nothing, Non refundable fare taxes
ONE-505.2	Proven	Full refund returns the whole price, Refund over journey
ONE-505.3	Proven	Fixed refund returns its amount, Refund over journey
ONE-505.4	Proven	Refund to the original form of payment, Refund over journey
ONE-505.5	Open	Full marked with amount, Taxes on a non-refundable fare, Non refundable fare taxes

34.2. Guarantees🔗

34.2.1. Forbidden cancellation returns nothing🔗

guarantee

Rules.OneOrder.Offers.cancel_forbidden_nothing
  (e : Rules.OneOrder.Offers.ExpiryReading)
  (ff : Rules.OneOrder.Offers.FullOrFixed)
  (rules : List Rules.OneOrder.Offers.Restriction)
  (j : Rules.OneOrder.Offers.Journey) (now : Rules.Core.Instant)
  (item : Rules.OneOrder.Offers.CancelledItem)
  (r : Rules.OneOrder.Offers.Restriction)
  (h :
    Rules.OneOrder.Offers.ruleInForce e rules j
        Rules.OneOrder.Offers.Action.cancel now =
      some r)
  (hr : r.allowed = false) :
  ∃ o,
    Rules.OneOrder.Offers.cancellationRefund e ff rules j now item =
      Rules.OneOrder.Offers.RefundDecision.refund
        { amount := 0, currency := item.price.currency } o
Rules.OneOrder.Offers.cancel_forbidden_nothing
  (e :
    Rules.OneOrder.Offers.ExpiryReading)
  (ff : Rules.OneOrder.Offers.FullOrFixed)
  (rules :
    List
      Rules.OneOrder.Offers.Restriction)
  (j : Rules.OneOrder.Offers.Journey)
  (now : Rules.Core.Instant)
  (item :
    Rules.OneOrder.Offers.CancelledItem)
  (r : Rules.OneOrder.Offers.Restriction)
  (h :
    Rules.OneOrder.Offers.ruleInForce e
        rules j
        Rules.OneOrder.Offers.Action.cancel
        now =
      some r)
  (hr : r.allowed = false) :
  ∃ o,
    Rules.OneOrder.Offers.cancellationRefund
        e ff rules j now item =
      Rules.OneOrder.Offers.RefundDecision.refund
        { amount := 0,
          currency :=
            item.price.currency }
        o

A cancellation the rule in force forbids returns nothing.

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

Checks acceptance criteria ONE-505.1.

34.2.2. Full refund returns the whole price🔗

guarantee

Rules.OneOrder.Offers.cancel_full_refund
  (e : Rules.OneOrder.Offers.ExpiryReading)
  (ff : Rules.OneOrder.Offers.FullOrFixed)
  (rules : List Rules.OneOrder.Offers.Restriction)
  (j : Rules.OneOrder.Offers.Journey) (now : Rules.Core.Instant)
  (item : Rules.OneOrder.Offers.CancelledItem)
  (r : Rules.OneOrder.Offers.Restriction)
  (h :
    Rules.OneOrder.Offers.ruleInForce e rules j
        Rules.OneOrder.Offers.Action.cancel now =
      some r)
  (hr : r.allowed = true)
  (hf : r.refund = Rules.OneOrder.Offers.RefundTerms.full) :
  ∃ o,
    Rules.OneOrder.Offers.cancellationRefund e ff rules j now item =
      Rules.OneOrder.Offers.RefundDecision.refund item.price o
Rules.OneOrder.Offers.cancel_full_refund
  (e :
    Rules.OneOrder.Offers.ExpiryReading)
  (ff : Rules.OneOrder.Offers.FullOrFixed)
  (rules :
    List
      Rules.OneOrder.Offers.Restriction)
  (j : Rules.OneOrder.Offers.Journey)
  (now : Rules.Core.Instant)
  (item :
    Rules.OneOrder.Offers.CancelledItem)
  (r : Rules.OneOrder.Offers.Restriction)
  (h :
    Rules.OneOrder.Offers.ruleInForce e
        rules j
        Rules.OneOrder.Offers.Action.cancel
        now =
      some r)
  (hr : r.allowed = true)
  (hf :
    r.refund =
      Rules.OneOrder.Offers.RefundTerms.full) :
  ∃ o,
    Rules.OneOrder.Offers.cancellationRefund
        e ff rules j now item =
      Rules.OneOrder.Offers.RefundDecision.refund
        item.price o

A cancellation the rule in force allows with a full refund and no fixed amount returns the item's whole price.

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

Checks acceptance criteria ONE-505.2.

34.2.3. Fixed refund returns its amount🔗

guarantee

Rules.OneOrder.Offers.cancel_fixed_refund
  (e : Rules.OneOrder.Offers.ExpiryReading)
  (ff : Rules.OneOrder.Offers.FullOrFixed)
  (rules : List Rules.OneOrder.Offers.Restriction)
  (j : Rules.OneOrder.Offers.Journey) (now : Rules.Core.Instant)
  (item : Rules.OneOrder.Offers.CancelledItem)
  (r : Rules.OneOrder.Offers.Restriction)
  (h :
    Rules.OneOrder.Offers.ruleInForce e rules j
        Rules.OneOrder.Offers.Action.cancel now =
      some r)
  (hr : r.allowed = true) (m : Rules.Core.Money)
  (hf : r.refund = Rules.OneOrder.Offers.RefundTerms.fixed m) :
  ∃ o,
    Rules.OneOrder.Offers.cancellationRefund e ff rules j now item =
      Rules.OneOrder.Offers.RefundDecision.refund m o
Rules.OneOrder.Offers.cancel_fixed_refund
  (e :
    Rules.OneOrder.Offers.ExpiryReading)
  (ff : Rules.OneOrder.Offers.FullOrFixed)
  (rules :
    List
      Rules.OneOrder.Offers.Restriction)
  (j : Rules.OneOrder.Offers.Journey)
  (now : Rules.Core.Instant)
  (item :
    Rules.OneOrder.Offers.CancelledItem)
  (r : Rules.OneOrder.Offers.Restriction)
  (h :
    Rules.OneOrder.Offers.ruleInForce e
        rules j
        Rules.OneOrder.Offers.Action.cancel
        now =
      some r)
  (hr : r.allowed = true)
  (m : Rules.Core.Money)
  (hf :
    r.refund =
      Rules.OneOrder.Offers.RefundTerms.fixed
        m) :
  ∃ o,
    Rules.OneOrder.Offers.cancellationRefund
        e ff rules j now item =
      Rules.OneOrder.Offers.RefundDecision.refund
        m o

A cancellation the rule in force allows with a fixed refund not marked full returns that amount.

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

Checks acceptance criteria ONE-505.3.

34.2.4. Refund to the original form of payment🔗

guarantee

Rules.OneOrder.Offers.cancel_to_original_form
  (e : Rules.OneOrder.Offers.ExpiryReading)
  (ff : Rules.OneOrder.Offers.FullOrFixed)
  (rules : List Rules.OneOrder.Offers.Restriction)
  (j : Rules.OneOrder.Offers.Journey) (now : Rules.Core.Instant)
  (item : Rules.OneOrder.Offers.CancelledItem)
  (r : Rules.OneOrder.Offers.Restriction)
  (h :
    Rules.OneOrder.Offers.ruleInForce e rules j
        Rules.OneOrder.Offers.Action.cancel now =
      some r)
  (hr : r.allowed = true) (ho : r.toOriginalForm = true) :
  ∃ m,
    Rules.OneOrder.Offers.cancellationRefund e ff rules j now item =
      Rules.OneOrder.Offers.RefundDecision.refund m true
Rules.OneOrder.Offers.cancel_to_original_form
  (e :
    Rules.OneOrder.Offers.ExpiryReading)
  (ff : Rules.OneOrder.Offers.FullOrFixed)
  (rules :
    List
      Rules.OneOrder.Offers.Restriction)
  (j : Rules.OneOrder.Offers.Journey)
  (now : Rules.Core.Instant)
  (item :
    Rules.OneOrder.Offers.CancelledItem)
  (r : Rules.OneOrder.Offers.Restriction)
  (h :
    Rules.OneOrder.Offers.ruleInForce e
        rules j
        Rules.OneOrder.Offers.Action.cancel
        now =
      some r)
  (hr : r.allowed = true)
  (ho : r.toOriginalForm = true) :
  ∃ m,
    Rules.OneOrder.Offers.cancellationRefund
        e ff rules j now item =
      Rules.OneOrder.Offers.RefundDecision.refund
        m true

A cancellation the rule in force allows, with the refund sent to the original form of payment, is refunded to the original form of payment.

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

Checks acceptance criteria ONE-505.4.

34.2.5. Taxes on a non-refundable fare🔗

guarantee

Rules.OneOrder.Offers.cancel_returns_refundable_charges
  (e : Rules.OneOrder.Offers.ExpiryReading)
  (ff : Rules.OneOrder.Offers.FullOrFixed)
  (rules : List Rules.OneOrder.Offers.Restriction)
  (j : Rules.OneOrder.Offers.Journey) (now : Rules.Core.Instant)
  (item : Rules.OneOrder.Offers.CancelledItem) (m : Rules.Core.Money)
  (o : Bool)
  (h :
    Rules.OneOrder.Offers.cancellationRefund e ff rules j now item =
      Rules.OneOrder.Offers.RefundDecision.refund m o) :
  item.refundableCharges ≤ m.amount
Rules.OneOrder.Offers.cancel_returns_refundable_charges
  (e :
    Rules.OneOrder.Offers.ExpiryReading)
  (ff : Rules.OneOrder.Offers.FullOrFixed)
  (rules :
    List
      Rules.OneOrder.Offers.Restriction)
  (j : Rules.OneOrder.Offers.Journey)
  (now : Rules.Core.Instant)
  (item :
    Rules.OneOrder.Offers.CancelledItem)
  (m : Rules.Core.Money) (o : Bool)
  (h :
    Rules.OneOrder.Offers.cancellationRefund
        e ff rules j now item =
      Rules.OneOrder.Offers.RefundDecision.refund
        m o) :
  item.refundableCharges ≤ m.amount

A voluntary cancellation of an unused item returns at least the taxes, fees and charges in its price that are flagged refundable.

Open question for the business. The guide gives each tax, fee and charge its own refund flag and gives each offer item cancel rules, and never says how the two combine. The rule returns what the cancel rule gives, so a rule that forbids cancellation returns nothing, and a fixed refund can be less than the refundable taxes. The examples nonRefundableFareTaxes and fullMarkedWithAmount show both. Does a cancel rule that returns nothing also keep the taxes flagged refundable, and does a no show change the answer?

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

Checks acceptance criteria ONE-505.5.

34.3. Examples🔗

34.3.1. Non refundable fare taxes🔗

example

Rules.OneOrder.Offers.nonRefundableFareTaxes :
  List Rules.OneOrder.Offers.RefundRow
Rules.OneOrder.Offers.nonRefundableFareTaxes :
  List Rules.OneOrder.Offers.RefundRow

Given the journey, its cancel rules and the trip at 500.00 EUR with a refundable airport tax of 25.00 EUR.

When the customer cancels on 25 January, and a customer who did not show up for the flight cancels on 2 February.

Then both cancellations return nothing, since the rule in force forbids cancellation, and the refundable airport tax is kept with the fare.

What Lean computed:

Case	Decision	Refundable charges
25 January	refund 0.00 EUR no	25.00 EUR
2 February, after a no show	refund 0.00 EUR no	25.00 EUR

Checks acceptance criteria ONE-505.1, ONE-505.5.

34.3.2. Refund over journey🔗

example

Rules.OneOrder.Offers.refundOverJourney :
  List Rules.OneOrder.Offers.RefundRow
Rules.OneOrder.Offers.refundOverJourney :
  List Rules.OneOrder.Offers.RefundRow

Given the journey, its cancel rules and the trip at 500.00 EUR with a refundable airport tax of 25.00 EUR.

When the customer cancels on 10 January and on 22 January.

Then on 10 January the whole 500.00 EUR is returned to the original form of payment. On 22 January the fixed 100.00 EUR is returned, and not to the original form of payment.

What Lean computed:

Case	Decision	Refundable charges
10 January	refund 500.00 EUR yes	25.00 EUR
22 January	refund 100.00 EUR no	25.00 EUR

Checks acceptance criteria ONE-505.2, ONE-505.3, ONE-505.4.

34.3.3. Full marked with amount🔗

example

Rules.OneOrder.Offers.fullMarkedWithAmount :
  List Rules.OneOrder.Offers.FullOrFixedRow
Rules.OneOrder.Offers.fullMarkedWithAmount :
  List
    Rules.OneOrder.Offers.FullOrFixedRow

Given the trip at 500.00 EUR with a refundable airport tax of 25.00 EUR, and a cancel rule that marks its refund as full and also gives a fixed amount of 1.00 EUR. One example in the guide has a rule like this.

When the customer cancels on 10 January, under each reading of the guide.

Then reading the refund as full returns 500.00 EUR. Reading it as the fixed amount returns 1.00 EUR, less than the refundable airport tax.

What Lean computed:

Reading	Decision	Refundable charges
full	refund 500.00 EUR no	25.00 EUR
fixed	refund 1.00 EUR no	25.00 EUR

Checks acceptance criteria ONE-505.5.

34.4. Open question🔗

The guarantee Taxes on a non-refundable fare is open: the example Non refundable fare taxes, Full marked with amount shows the rule as written breaking it. Questions from the ONE Order rules sets out the question for the team.