1
における機能の終了
証明します。資料はthisの5ページ目です。この関数は、正規表現（Isabelle/HOLで形式化されています）の正規化関数の一部として実行されます。 le_regex関数は同じ論文から適合されています。私は決定的な合計順序でregexのパラメータ化を避けるためにasciiを使用しています（プログラムを抽出したい）。は、私はトラブル次の関数の終了を証明を持っていますCoqの
Inductive regex : Set :=
| Empty : regex
| Epsilon : regex
| Symbol : ascii -> regex
| Union : regex -> regex -> regex
| Concat : regex -> regex -> regex
| Star : regex -> regex.
Lemma eq_regex_dec : forall u v : regex, {u = v} + {u <> v}.
Proof. decide equality; apply ascii_dec. Defined.
Fixpoint le_regex u v : bool :=
match u, v with
| Empty , _ => true
| _ , Empty => false
| Epsilon , _ => true
| _ , Epsilon => false
| Symbol a , Symbol b => nat_of_ascii a <=? nat_of_ascii b
| Symbol _ , _ => true
| _ , Symbol _ => false
| Star u , Star v => le_regex u v
| Star u , _ => true
| _ , Star v => false
| Union u1 u2 , Union v1 v2 => if eq_regex_dec u1 v1
then le_regex u2 v2
else le_regex u1 v1
| Union _ _ , _ => true
| _ , Union _ _ => false
| Concat u1 u2, Concat v1 v2 => if eq_regex_dec u1 v1
then le_regex u2 v2
else le_regex u1 v1
end.
私は正しいアプローチは減少メジャーを定義し、終了を証明するためにProgram Fixpointを使用することだと思います。しかし、私は正しい対策（オペレータの数に基づく試行が失敗した）を考え出すのに問題があります。私は仕事を別々の機能に分解しようとしましたが、同様の問題に遭遇しました。どんな援助も感謝されるでしょう、または正しい方向を指すヒント。私はあなたがタイプregexに値を返すべきではないことを示唆している
Union u v, w => norm_union u (norm_union v w) (* line 5 *)
：あなたは次の行では、ネストされた再帰呼び出しを持っているので、
正規表現の定義を質問の一部としてCoq構文で追加してください。 – Yves