C++20 Concepts constraints subsumption analysis

subsume-P0717R1.txt

constraint-expressions:
- C1<T>^c && C2<T>^c
- C1<T>^d

# concept version
template <class T> concept C1<T> = true^a;
template <class T> concept C2<T> = true^b;

normal form of P = true^a ∧ true^b
normal form of Q = true^a

P_1 = (true^a ∧ true^b)
Q_1 = (true^a)
  ⇒ P_11=(true^a) identical Q_11=(true^a) ⇒ P_11 subsume Q_11
  ⇒ (true^a && true^b) subsume (true^a)

normal form of P = true^a
normal form of Q = true^a ∧ true^b

P_1 = (true^a)
Q_1 = (true^a), Q_2=(true^b)
  { P_11=(true^a)     identical Q_11=(true^a) ⇒ P_11     subsume Q_11,
    P_11=(true^a) NOT identical Q_21=(true^b) ⇒ P_11 NOT subsume Q_21 }
  ⇒ (true^a) NOT subsume (true^a && true^b)


# non-concept version
template <class T> inline constexpr bool C1<T> = true^a;
template <class T> inline constexpr bool C2<T> = true^b;

normal form of P = C1<T>^c ∧ C2<T>^c
normal form of Q = C1<T>^d

P_1 = (C1<T>^c ∧ C2<T>^c)
Q_1 = (C1<T>^d)
  { P_11=(C1<T>^c) NOT identical Q_11=(C1<T>^c) ⇒ P_11 NOT subsume Q_11,
  { P_12=(C2<T>^c) NOT identical Q_11=(C1<T>^c) ⇒ P_12 NOT subsume Q_11 }
  ⇒ (C1<T>^c && C2<T>^c) NOT subsume (C1<T>^d)

normal form of P = C1<T>^d
normal form of Q = C1<T>^c ∧ C2<T>^c

P_1 = (C1<T>^d)
Q_1 = (C1<T>^c), Q_2 = (C2<T>^c)
  { P_11=(C1<T>^d) NOT identical Q_11=(C1<T>^c) ⇒ P_11 NOT subsume Q_11,
    P_11=(C1<T>^d) NOT identical Q_21=(C2<T>^c) ⇒ P_11 NOT subsume Q_21 }
  ⇒ (C1<T>^d) NOT subsume (C1<T>^c && C2<T>^c)

subsume-wrong.txt

constraint-expressions:
- C1<T> && C2<T>
- C1<T>

# concept version
template <class T> concept C1<T> = true;
template <class T> concept C2<T> = true;

normal form of P = true ∧ true
normal form of Q = true

P_1 = (true ∧ true)
Q_1 = (true)
  ⇒ P_11=(true) identical Q_11=(true) ⇒ P_11 subsume Q_11
  ⇒ (true && true) subsume (true)

normal form of P = true
normal form of Q = true ∧ true

P_1 = (true)
Q_1 = (true), Q_2=(true)
  { P_11=(true) identical Q_11=(true) ⇒ P_11 subsume Q_11,
    P_11=(true) identical Q_21=(true) ⇒ P_11 subsume Q_21 }
  ⇒ true subsume (true && true)


# non-concept version
template <class T> inline constexpr bool C1<T> = true;
template <class T> inline constexpr bool C2<T> = true;

normal form of P = C1<T> ∧ C2<T>
normal form of Q = C1<T>

P_1 = (C1<T> ∧ C2<T>)
Q_1 = (C1<T>)
  ⇒ P_11=(C1<T>) identical Q_11=(C1<T>) ⇒ P_11 subsume Q_11
  ⇒ (C1<T> && C2<T>) subsume (C1<T>)

normal form of P = C1<T>
normal form of Q = C1<T> ∧ C2<T>

P_1 = (C1<T>)
Q_1 = (C1<T>), Q_2 = (C2<T>)
  { P_11=(C1<T>)     identical Q_11=(C1<T>) ⇒ P_11     subsume Q_11,
    P_11=(C1<T>) NOT identical Q_21=(C2<T>) ⇒ P_11 NOT subsume Q_21 }
  ⇒ C1<T> NOT subsume (C1<T> && C2<T>)

related: https://yohhoy.hatenadiary.jp/entry/20190903/p1 (ja)