From 5e8718dff9d7906e1d4ca7020256dae7c05e49c2 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 30 Sep 2024 16:31:10 +1000 Subject: [PATCH] chore: fix Array.modify lemmas (#5536) Generally works best to pick up the proofs by unification with the lhs. pinging @hargoniX as this goes by, as it changes some proofs in bv_decide (nothing interesting, just a bit simpler) --- src/Init/Data/Array/Lemmas.lean | 24 +++++----- .../LRAT/Internal/Formula/Lemmas.lean | 32 ++++++------- .../LRAT/Internal/Formula/RupAddResult.lean | 45 ++++++++----------- .../LRAT/Internal/Formula/RupAddSound.lean | 15 +++---- 4 files changed, 51 insertions(+), 65 deletions(-) diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean index 64c8cc6d0b..7993021816 100644 --- a/src/Init/Data/Array/Lemmas.lean +++ b/src/Init/Data/Array/Lemmas.lean @@ -871,26 +871,26 @@ theorem mapIdx_spec (as : Array α) (f : Fin as.size → α → β) unfold modify modifyM Id.run split <;> simp -theorem getElem_modify {as : Array α} {x i} (h : i < as.size) : - (as.modify x f)[i]'(by simp [h]) = if x = i then f as[i] else as[i] := by +theorem getElem_modify {as : Array α} {x i} (h : i < (as.modify x f).size) : + (as.modify x f)[i] = if x = i then f (as[i]'(by simpa using h)) else as[i]'(by simpa using h) := by simp only [modify, modifyM, get_eq_getElem, Id.run, Id.pure_eq] split - · simp only [Id.bind_eq, get_set _ _ _ h]; split <;> simp [*] - · rw [if_neg (mt (by rintro rfl; exact h) ‹_›)] + · simp only [Id.bind_eq, get_set _ _ _ (by simpa using h)]; split <;> simp [*] + · rw [if_neg (mt (by rintro rfl; exact h) (by simp_all))] -theorem getElem_modify_self {as : Array α} {i : Nat} (h : i < as.size) (f : α → α) : - (as.modify i f)[i]'(by simp [h]) = f as[i] := by +theorem getElem_modify_self {as : Array α} {i : Nat} (f : α → α) (h : i < (as.modify i f).size) : + (as.modify i f)[i] = f (as[i]'(by simpa using h)) := by simp [getElem_modify h] -theorem getElem_modify_of_ne {as : Array α} {i : Nat} (hj : j < as.size) - (f : α → α) (h : i ≠ j) : - (as.modify i f)[j]'(by rwa [size_modify]) = as[j] := by +theorem getElem_modify_of_ne {as : Array α} {i : Nat} (h : i ≠ j) + (f : α → α) (hj : j < (as.modify i f).size) : + (as.modify i f)[j] = as[j]'(by simpa using hj) := by simp [getElem_modify hj, h] @[deprecated getElem_modify (since := "2024-08-08")] -theorem get_modify {arr : Array α} {x i} (h : i < arr.size) : - (arr.modify x f).get ⟨i, by simp [h]⟩ = - if x = i then f (arr.get ⟨i, h⟩) else arr.get ⟨i, h⟩ := by +theorem get_modify {arr : Array α} {x i} (h : i < (arr.modify x f).size) : + (arr.modify x f).get ⟨i, h⟩ = + if x = i then f (arr.get ⟨i, by simpa using h⟩) else arr.get ⟨i, by simpa using h⟩ := by simp [getElem_modify h] /-! ### filter -/ diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean index a1af5c912e..c6bcc304f4 100644 --- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean +++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean @@ -136,12 +136,10 @@ theorem readyForRupAdd_ofArray {n : Nat} (arr : Array (Option (DefaultClause n)) exact ih.2 i b h | some (l, true) => simp only [heq] at h - have i_in_bounds : i.1 < acc.size := by simp only [ih.1, i.2.2] - have l_in_bounds : l.1 < acc.size := by simp only [ih.1, l.2.2] rcases ih with ⟨hsize, ih⟩ by_cases i = l.1 · next i_eq_l => - simp only [i_eq_l, Array.getElem_modify_self l_in_bounds] at h + simp only [i_eq_l, Array.getElem_modify_self] at h by_cases b · next b_eq_true => rw [isUnit_iff, DefaultClause.toList] at heq @@ -160,16 +158,14 @@ theorem readyForRupAdd_ofArray {n : Nat} (arr : Array (Option (DefaultClause n)) rw [b_eq_false, Subtype.ext i_eq_l] exact ih h · next i_ne_l => - simp only [Array.getElem_modify_of_ne i_in_bounds _ (Ne.symm i_ne_l)] at h + simp only [Array.getElem_modify_of_ne (Ne.symm i_ne_l)] at h exact ih i b h | some (l, false) => simp only [heq] at h - have i_in_bounds : i.1 < acc.size := by simp only [ih.1, i.2.2] - have l_in_bounds : l.1 < acc.size := by simp only [ih.1, l.2.2] rcases ih with ⟨hsize, ih⟩ by_cases i = l.1 · next i_eq_l => - simp only [i_eq_l, Array.getElem_modify_self l_in_bounds] at h + simp only [i_eq_l, Array.getElem_modify_self] at h by_cases b · next b_eq_true => simp only [hasAssignment, b_eq_true, ite_true, hasPos_addNeg] at h @@ -187,7 +183,7 @@ theorem readyForRupAdd_ofArray {n : Nat} (arr : Array (Option (DefaultClause n)) rw [c_def] at cOpt_in_arr exact cOpt_in_arr · next i_ne_l => - simp only [Array.getElem_modify_of_ne i_in_bounds _ (Ne.symm i_ne_l)] at h + simp only [Array.getElem_modify_of_ne (Ne.symm i_ne_l)] at h exact ih i b h rcases List.foldlRecOn arr.toList ofArray_fold_fn (mkArray n unassigned) hb hl with ⟨_h_size, h'⟩ intro i b h @@ -281,7 +277,6 @@ theorem readyForRupAdd_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClaus intro i b hb have hf := f_readyForRupAdd.2.2 i b have i_in_bounds : i.1 < f.assignments.size := by rw [f_readyForRupAdd.2.1]; exact i.2.2 - have l_in_bounds : l.1 < f.assignments.size := by rw [f_readyForRupAdd.2.1]; exact l.2.2 simp only at hb by_cases (i, b) = (l, true) · next ib_eq_c => @@ -292,7 +287,7 @@ theorem readyForRupAdd_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClaus apply DefaultClause.ext simp only [unit, hc] · next ib_ne_c => - have hb' : hasAssignment b (f.assignments[i.1]'i_in_bounds) := by + have hb' : hasAssignment b f.assignments[i.1] := by by_cases l.1 = i.1 · next l_eq_i => have b_eq_false : b = false := by @@ -302,10 +297,10 @@ theorem readyForRupAdd_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClaus · next b_eq_false => simp only [Bool.not_eq_true] at b_eq_false exact b_eq_false - simp only [hasAssignment, b_eq_false, l_eq_i, Array.getElem_modify_self i_in_bounds, ite_false, hasNeg_addPos, reduceCtorEq] at hb + simp only [hasAssignment, b_eq_false, l_eq_i, Array.getElem_modify_self, ite_false, hasNeg_addPos, reduceCtorEq] at hb simp only [hasAssignment, b_eq_false, ite_false, hb, reduceCtorEq] · next l_ne_i => - simp only [Array.getElem_modify_of_ne i_in_bounds _ l_ne_i] at hb + simp only [Array.getElem_modify_of_ne l_ne_i] at hb exact hb specialize hf hb' simp only [toList, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq, @@ -322,7 +317,6 @@ theorem readyForRupAdd_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClaus intro i b hb have hf := f_readyForRupAdd.2.2 i b have i_in_bounds : i.1 < f.assignments.size := by rw [f_readyForRupAdd.2.1]; exact i.2.2 - have l_in_bounds : l.1 < f.assignments.size := by rw [f_readyForRupAdd.2.1]; exact l.2.2 simp only at hb by_cases (i, b) = (l, false) · next ib_eq_c => @@ -333,7 +327,7 @@ theorem readyForRupAdd_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClaus apply DefaultClause.ext simp only [unit, hc] · next ib_ne_c => - have hb' : hasAssignment b (f.assignments[i.1]'i_in_bounds) := by + have hb' : hasAssignment b f.assignments[i.1] := by by_cases l.1 = i.1 · next l_eq_i => have b_eq_false : b = true := by @@ -341,10 +335,10 @@ theorem readyForRupAdd_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClaus · assumption · next b_eq_false => simp only [b_eq_false, Subtype.ext l_eq_i, not_true] at ib_ne_c - simp only [hasAssignment, b_eq_false, l_eq_i, Array.getElem_modify_self i_in_bounds, ite_true, hasPos_addNeg] at hb + simp only [hasAssignment, b_eq_false, l_eq_i, Array.getElem_modify_self, ite_true, hasPos_addNeg] at hb simp only [hasAssignment, b_eq_false, ite_true, hb] · next l_ne_i => - simp only [Array.getElem_modify_of_ne i_in_bounds _ l_ne_i] at hb + simp only [Array.getElem_modify_of_ne l_ne_i] at hb exact hb specialize hf hb' simp only [toList, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq, @@ -471,14 +465,14 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor simp only [deleteOne, heq, hl] at hb by_cases l.1.1 = i.1 · next l_eq_i => - simp only [l_eq_i, Array.getElem_modify_self i_in_bounds] at hb + simp only [l_eq_i, Array.getElem_modify_self] at hb have l_ne_b : l.2 ≠ b := by intro l_eq_b rw [← l_eq_b] at hb have hb' := not_has_remove f.assignments[i.1] l.2 simp [hb] at hb' replace l_ne_b := Bool.eq_not_of_ne l_ne_b - rw [l_ne_b] at hb + simp only [l_ne_b] at hb have hb := has_remove_irrelevant f.assignments[i.1] b hb specialize hf i b hb simp only [toList, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq, @@ -512,7 +506,7 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor · exact hf · exact Or.inr hf · next l_ne_i => - simp only [Array.getElem_modify_of_ne i_in_bounds _ l_ne_i] at hb + simp only [Array.getElem_modify_of_ne l_ne_i] at hb specialize hf i b hb simp only [toList, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq, exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool] at hf diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean index 7a613b59da..b5994b39f8 100644 --- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean +++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean @@ -115,7 +115,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen constructor · rfl · constructor - · rw [Array.getElem_modify_self l_in_bounds] + · rw [Array.getElem_modify_self] simp only [← i_eq_l, h1] · constructor · simp only [getElem!, l_in_bounds, ↓reduceDIte, Array.get_eq_getElem, @@ -138,7 +138,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen · next i_ne_l => apply Or.inl simp only [insertUnit, h3, ite_false, reduceCtorEq] - rw [Array.getElem_modify_of_ne i_in_bounds _ (Ne.symm i_ne_l)] + rw [Array.getElem_modify_of_ne (Ne.symm i_ne_l)] constructor · exact h1 · intro j @@ -197,7 +197,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen rfl · constructor · simp only [i_eq_l] - rw [Array.getElem_modify_self l_in_bounds] + rw [Array.getElem_modify_self] simp only [addAssignment, hl, ← i_eq_l, h2, ite_true, ite_false] apply addNeg_addPos_eq_both · constructor @@ -234,7 +234,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen · rw [Array.get_push_lt units l j.1 j.2, h1] · constructor · simp only [i_eq_l] - rw [Array.getElem_modify_self l_in_bounds] + rw [Array.getElem_modify_self] simp only [addAssignment, hl, ← i_eq_l, h2, ite_true, ite_false] apply addPos_addNeg_eq_both · constructor @@ -277,7 +277,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen constructor · rw [Array.get_push_lt units l j.1 j.2, h1] · constructor - · rw [Array.getElem_modify_of_ne i_in_bounds _ (Ne.symm i_ne_l), h2] + · rw [Array.getElem_modify_of_ne (Ne.symm i_ne_l), h2] · constructor · exact h3 · intro k k_ne_j @@ -319,9 +319,9 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen by_cases i.1 = l.1.1 · next i_eq_l => simp only [i_eq_l] - rw [Array.getElem_modify_self l_in_bounds] + rw [Array.getElem_modify_self] simp only [← i_eq_l, h3, add_both_eq_both] - · next i_ne_l => rw [Array.getElem_modify_of_ne i_in_bounds _ (Ne.symm i_ne_l), h3] + · next i_ne_l => rw [Array.getElem_modify_of_ne (Ne.symm i_ne_l), h3] · constructor · exact h4 · intro k k_ne_j1 k_ne_j2 @@ -535,7 +535,7 @@ theorem clear_insert_inductive_case {n : Nat} (f : DefaultFormula n) (f_assignme have i_in_bounds : i.1 < assignments.size := by rw [hsize] exact i.2 - have h := Array.getElem_modify_of_ne i_in_bounds (removeAssignment units[idx.val].2) ih2 + have h := Array.getElem_modify_of_ne ih2 (removeAssignment units[idx.val].2) (by simpa using i_in_bounds) simp only [Fin.getElem_fin] at h rw [h] exact ih1 @@ -546,8 +546,7 @@ theorem clear_insert_inductive_case {n : Nat} (f : DefaultFormula n) (f_assignme apply Or.inl constructor · simp only [clearUnit, idx_eq_j, Array.get_eq_getElem, ih1] - have i_in_bounds : i.1 < assignments.size := by rw [hsize]; exact i.2 - rw [Array.getElem_modify_self i_in_bounds, ih2, remove_add_cancel] + rw [Array.getElem_modify_self, ih2, remove_add_cancel] exact ih3 · intro k k_ge_idx_add_one have k_ge_idx : k.val ≥ idx.val := Nat.le_of_succ_le k_ge_idx_add_one @@ -568,8 +567,7 @@ theorem clear_insert_inductive_case {n : Nat} (f : DefaultFormula n) (f_assignme · constructor · simp only [clearUnit, Array.get_eq_getElem] specialize ih4 idx (Nat.le_refl idx.1) idx_ne_j - have i_in_bounds : i.1 < assignments.size := by rw [hsize]; exact i.2 - rw [Array.getElem_modify_of_ne i_in_bounds _ ih4] + rw [Array.getElem_modify_of_ne ih4] exact ih2 · constructor · exact ih3 @@ -593,8 +591,7 @@ theorem clear_insert_inductive_case {n : Nat} (f : DefaultFormula n) (f_assignme exact ih2 · constructor · simp only [clearUnit, idx_eq_j1, Array.get_eq_getElem, ih1] - have i_in_bounds : i.1 < assignments.size := hsize ▸ i.2 - rw [Array.getElem_modify_self i_in_bounds, ih3, ih4] + rw [Array.getElem_modify_self, ih3, ih4] decide · constructor · simp [hasAssignment, hasNegAssignment, ih4] @@ -630,8 +627,7 @@ theorem clear_insert_inductive_case {n : Nat} (f : DefaultFormula n) (f_assignme exact ih1 · constructor · simp only [clearUnit, idx_eq_j2, Array.get_eq_getElem, ih2] - have i_in_bounds : i.1 < assignments.size := hsize ▸ i.2 - rw [Array.getElem_modify_self i_in_bounds, ih3, ih4] + rw [Array.getElem_modify_self, ih3, ih4] decide · constructor · simp only [hasAssignment, hasNegAssignment, ih4, ite_false, not_false_eq_true] @@ -687,10 +683,7 @@ theorem clear_insert_inductive_case {n : Nat} (f : DefaultFormula n) (f_assignme simp only [Bool.not_eq_true] at h2 simp only [Fin.getElem_fin, ih2, ← h1, ← h2, ne_eq] at h3 exact h3 rfl - have idx_unit_in_bounds : units[idx.1].1.1 < assignments.size := by - rw [hsize]; exact units[idx.1].1.2.2 - have i_in_bounds : i.1 < assignments.size := hsize ▸ i.2 - rw [Array.getElem_modify_of_ne i_in_bounds _ idx_res_ne_i] + rw [Array.getElem_modify_of_ne idx_res_ne_i] exact ih3 · constructor · exact ih4 @@ -796,7 +789,7 @@ theorem confirmRupHint_preserves_invariant_helper {n : Nat} (f : DefaultFormula constructor · simp only [List.get, l_eq_i] · constructor - · simp only [l_eq_i, Array.getElem_modify_self i_in_bounds, List.get, h1] + · simp only [l_eq_i, Array.getElem_modify_self, List.get, h1] · constructor · simp only [List.get, Bool.not_eq_true] simp only [getElem!, l_in_bounds, ↓reduceDIte, Array.get_eq_getElem, @@ -826,7 +819,7 @@ theorem confirmRupHint_preserves_invariant_helper {n : Nat} (f : DefaultFormula · next l_ne_i => apply Or.inl constructor - · rw [Array.getElem_modify_of_ne i_in_bounds (addAssignment l.2) l_ne_i] + · rw [Array.getElem_modify_of_ne l_ne_i] exact h1 · intro l' l'_in_list simp only [List.find?, List.mem_cons] at l'_in_list @@ -865,7 +858,7 @@ theorem confirmRupHint_preserves_invariant_helper {n : Nat} (f : DefaultFormula apply And.intro l_eq_true ∘ And.intro l'_eq_false constructor · simp only [l'] at l'_eq_false - simp only [l_eq_i, addAssignment, l_eq_true, ite_true, Array.getElem_modify_self i_in_bounds, h1, + simp only [l_eq_i, addAssignment, l_eq_true, ite_true, Array.getElem_modify_self, h1, l'_eq_false, ite_false] apply addPos_addNeg_eq_both · constructor @@ -914,7 +907,7 @@ theorem confirmRupHint_preserves_invariant_helper {n : Nat} (f : DefaultFormula apply And.intro l'_eq_true ∘ And.intro l_eq_false constructor · simp only [l'] at l'_eq_true - simp only [l_eq_i, addAssignment, l'_eq_true, ite_true, Array.getElem_modify_self i_in_bounds, h1, + simp only [l_eq_i, addAssignment, l'_eq_true, ite_true, Array.getElem_modify_self, h1, l_eq_false, ite_false] apply addNeg_addPos_eq_both · constructor @@ -950,7 +943,7 @@ theorem confirmRupHint_preserves_invariant_helper {n : Nat} (f : DefaultFormula constructor · exact j_eq_i · constructor - · rw [Array.getElem_modify_of_ne i_in_bounds _ l_ne_i] + · rw [Array.getElem_modify_of_ne l_ne_i] exact h1 · apply And.intro h2 intro k k_ne_j_succ @@ -1002,7 +995,7 @@ theorem confirmRupHint_preserves_invariant_helper {n : Nat} (f : DefaultFormula all_goals simp (config := {decide := true}) [getElem!, l_eq_i, i_in_bounds, h1, decidableGetElem?] at h constructor - · rw [Array.getElem_modify_of_ne i_in_bounds _ l_ne_i] + · rw [Array.getElem_modify_of_ne l_ne_i] exact h1 · constructor · exact h2 diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean index f82f9429b1..518d0f4552 100644 --- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean +++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean @@ -39,27 +39,26 @@ theorem contradiction_of_insertUnit_success {n : Nat} (assignments : Array Assig rcases insertUnit_success with foundContradiction_eq_true | assignments_l_ne_unassigned · simp only [insertUnit, hl, ite_false] rcases h foundContradiction_eq_true with ⟨i, h⟩ - have i_in_bounds : i.1 < assignments.size := by rw [assignments_size]; exact i.2.2 apply Exists.intro i by_cases l.1.1 = i.1 · next l_eq_i => - simp [l_eq_i, Array.getElem_modify_self i_in_bounds, h] + simp [l_eq_i, Array.getElem_modify_self, h] exact add_both_eq_both l.2 · next l_ne_i => - simp [Array.getElem_modify_of_ne i_in_bounds _ l_ne_i] + simp [Array.getElem_modify_of_ne l_ne_i] exact h · apply Exists.intro l.1 - simp only [insertUnit, hl, ite_false, Array.getElem_modify_self l_in_bounds, reduceCtorEq] + simp only [insertUnit, hl, ite_false, Array.getElem_modify_self, reduceCtorEq] simp only [getElem!, l_in_bounds, dite_true, decidableGetElem?] at assignments_l_ne_unassigned by_cases l.2 · next l_eq_true => - rw [l_eq_true] + simp only [l_eq_true] simp only [hasAssignment, l_eq_true, hasPosAssignment, getElem!, l_in_bounds, dite_true, ite_true, Bool.not_eq_true, decidableGetElem?] at hl split at hl <;> simp_all (config := { decide := true }) · next l_eq_false => simp only [Bool.not_eq_true] at l_eq_false - rw [l_eq_false] + simp only [l_eq_false] simp [hasAssignment, l_eq_false, hasNegAssignment, getElem!, l_in_bounds, decidableGetElem?] at hl split at hl <;> simp_all (config := { decide := true }) @@ -681,7 +680,7 @@ theorem confirmRupHint_preserves_motive {n : Nat} (f : DefaultFormula n) (rupHin by_cases l.1 = i.1 · next l_eq_i => simp only [getElem!, Array.size_modify, i_in_bounds, ↓ reduceDIte, - Array.get_eq_getElem, l_eq_i, Array.getElem_modify_self i_in_bounds (addAssignment b), decidableGetElem?] + Array.get_eq_getElem, l_eq_i, Array.getElem_modify_self (addAssignment b), decidableGetElem?] simp only [getElem!, i_in_bounds, dite_true, Array.get_eq_getElem, decidableGetElem?] at pacc by_cases pi : p i · simp only [pi, decide_False] @@ -705,7 +704,7 @@ theorem confirmRupHint_preserves_motive {n : Nat} (f : DefaultFormula n) (rupHin exact pacc · next l_ne_i => simp only [getElem!, Array.size_modify, i_in_bounds, - Array.getElem_modify_of_ne i_in_bounds _ l_ne_i, dite_true, + Array.getElem_modify_of_ne l_ne_i, dite_true, Array.get_eq_getElem, decidableGetElem?] simp only [getElem!, i_in_bounds, dite_true, decidableGetElem?] at pacc exact pacc